Least Fixpoint and Greatest Fixpoint in a Process Algebra with Conjunction and Disjunction

Yoshinao ISOBE  Yutaka SATO  Kazuhito OHMAKI  

Publication
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences   Vol.E83-A   No.3   pp.401-411
Publication Date: 2000/03/25
Online ISSN: 
DOI: 
Print ISSN: 0916-8508
Type of Manuscript: Special Section PAPER (Special Section of Selected Papers from the 12th Workshop on Circuits and Systems in Karuizawa)
Category: 
Keyword: 
process algebra,  process logic,  process synthesis,  least fixpoint,  greatest fixpoint,  

Full Text: PDF(584.4KB)>>
Buy this Article



Summary: 
We have already proposed a process algebra µLOTOS as a mathematical framework to synthesize a 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 . In this paper, we present µLOTOSR, which is a refined µLOTOS. The improvement is that µLOTOSR has a conjunction operator . Therefore, the consistency between a number of specifications S1,,S2 can be checked by the satisfiability of the conjunction specification S1 S2. µLOTOSR does not need the complex consistency check used in µLOTOS.