Equation solving using modal transition systems
- 4 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 108-117
- https://doi.org/10.1109/lics.1990.113738
Abstract
This research offers as its main contribution a complete treatment of equation solving within process algebra for equation systems of the following form: C/sub 1/(X) approximately P/sub 1/, . . ., C/sub n(X)/ approximately P/sub n/ where C/sub i/ are arbitrary contexts (i.e. derived operators) of some process algebra, P/sub i/ are arbitrary process (i.e. terms of the process algebra), approximately is the bisimulation equivalence, and X is the unknown process to be found (if possible). It is shown that the solution set to this equation may be characterized in terms of a distinctive modal transition system, and that a solution to the above equation systems may be readily extracted (when solutions exist) on this basis. In fact, the results have led to an implementation (in Prolog) of an automatic tool for solving equations in the finite-state case.Keywords
This publication has 18 references indexed in Scilit:
- Compositionality through an operational semantics of contextsPublished by Springer Nature ,2005
- Proof systems for Hennessy-Milner Logic with recursionPublished by Springer Nature ,2005
- Linear and branching structures in the semantics and logics of reactive systemsPublished by Springer Nature ,2005
- A modal process logicPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- The concurrency workbenchPublished by Springer Nature ,1990
- Modal specificationsPublished by Springer Nature ,1990
- The use of static constructs in a model process logicLecture Notes in Computer Science, 1989
- Algebraic laws for nondeterminism and concurrencyJournal of the ACM, 1985
- Using branching time temporal logic to synthesize synchronization skeletonsScience of Computer Programming, 1982
- Communicating sequential processesCommunications of the ACM, 1978