Compositional minimisation of finite state systems using interface specifications
- 1 September 1996
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 8 (5), 607-616
- https://doi.org/10.1007/bf01211911
Abstract
We present a method for the compositional construction of the minimal transition system that represents the semantics of a given distributed system. Our aim is to control the state explosion caused by the interleavings of actions of communicating parallel components by reduction steps that exploit global communication constraints given in terms of interface specifications. The effect of the method, which is developed for bisimulation semantics here, depends on the structure of the distributed system under consideration, and the accuracy of the interface specifications. However, its correctness is independent of the correctness of the interface specifications provided by the program designer.Keywords
This publication has 17 references indexed in Scilit:
- Compositional proofs by partial specification of processesPublished by Springer Science and Business Media LLC ,2005
- Minimal model generationPublished by Springer Science and Business Media LLC ,2005
- The modular framework of computer-aided verificationPublished by Springer Science and Business Media LLC ,2005
- Compositional minimisation of finite state systems using interface specificationsFormal Aspects of Computing, 1996
- Property preserving abstractions for the verification of concurrent systemsFormal Methods in System Design, 1995
- All from one, one for all: on model checking using representativesLecture Notes in Computer Science, 1993
- On-the-fly verification with stubborn setsLecture Notes in Computer Science, 1993
- Some observations on redundancy in a contextPublished by Cambridge University Press (CUP) ,1990
- MCTL — An extension of CTL for modular verification of concurrent systemsPublished by Springer Science and Business Media LLC ,1989
- In Transition From Global to Modular Temporal Reasoning about ProgramsPublished by Springer Science and Business Media LLC ,1985