For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Least Fixpoint and Greatest Fixpoint in a Process Algebra with Conjunction and Disjunction
Yoshinao ISOBE Yutaka SATO Kazuhito OHMAKI
IEICE TRANSACTIONS on Fundamentals of Electronics, Communications and Computer Sciences
Publication Date: 2000/03/25
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)
process algebra, process logic, process synthesis, least fixpoint, greatest fixpoint,
Full Text: PDF(584.4KB)>>
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.