Least Fixpoint and Greatest Fixpoint in a Process Algebra with Conjunction and Disjunction (Special Section of Selected Papers from the 12th Workshop on Circuit and Systems in Karuizawa)

概要

論文の詳細を見る
We have already proposed a process algebra μLOTOS as a mathematical framework to synthesizea process from a number of (incomplete) specifications, in which requirements for the process do not have to be completely determined. It is guaranteed that the synthesized process satisfies all the given specifications, if they are consistent. For example, μLOTOS is useful for incremental design. The advantage of μLOTOS is that liveness properties can be expressed by least fixpoints and disjunctions V. In this paper, we present μLOTOS^R which is a refined μLOTOS. The improvement is that μLOTOS^R has a conjunction operator Λ. Therefore, the consistency between a number of specifications S_1, ・・・, S_2 can be checked by the satisfiability of the conjuction specification S_1 Λ ・・・ Λ S_2. μLOTOS^R does not need the complex consistency check used in μLOTOS.
一般社団法人電子情報通信学会の論文
2000-03-25