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 thecompositional constructionof theminimal transition systemthat represents the semantics of a given distributed system. Our aim is to control thestate explosioncaused by the interleavings of actions of communicating parallel components byreduction stepsthat exploitglobalcommunication constraints given in terms ofinterface specifications.Theeffectof the method, which is developed forbisimulation semanticshere, depends on the structure of the distributed system under consideration, and theaccuracyof the interface specifications. However, itscorrectnessis 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 Nature ,2005
- Minimal model generationPublished by Springer Nature ,2005
- The modular framework of computer-aided verificationPublished by Springer Nature ,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 representativesPublished by Springer Nature ,1993
- On-the-fly verification with stubborn setsPublished by Springer Nature ,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 Nature ,1989
- In Transition From Global to Modular Temporal Reasoning about ProgramsPublished by Springer Nature ,1985