Abstract
We present a method for thecompositional construction of theminimal transition system that represents the semantics of a given distributed system. Our aim is to control thestate explosion caused by the interleavings of actions of communicating parallel components byreduction steps that exploitglobal communication constraints given in terms ofinterface specifications. Theeffect of the method, which is developed forbisimulation semantics here, depends on the structure of the distributed system under consideration, and theaccuracy of the interface specifications. However, itscorrectness is independent of the correctness of the interface specifications provided by the program designer.
Similar content being viewed by others
References
Bouajjani, A., Fernandez, J.-C. and Halbwachs, N.: Minimal model generation. InWorkshop on Automatic Verification '90, volume 531 ofLNCS, 1990.
Clarke, E., Grumberg, O. and Long, D.: Model checking and abstraction. InSymp. Principles of Programming Languages '92, 1992.
Clarke, E., Long, D. and McMillan, K.: Compositional model checking.Proc. IEEE Symp. Logic in Computer Science, pages 353–362, 1989.
Cleaveland, R. and Steffen, B.: A preorder for partial process specifications. InProceedings of CONCUR'90, Amsterdam (Netherlands), volume 458 ofLNCS, 1990.
Dams, D., Grumberg, O. and Gerth, R.: Generation of reduced models for checking fragments of CTL. InProceedings of the International Conference on Computer-Aided Verification (CAV'93), volume 697of LNCS, pages 479–490, 1993.
Fernandez, J.-C.:Aldébaran: Un Système de Vérification par Réduction de Processus Communicants. PhD thesis, Université de Grenoble, 1988.
Godefroid, P. and Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. InProceedings of the International Workshop on Computer-Aided Verification (CAV'91), volume 575of LNCS, pages 332–342, 1991.
Graf, S., Steffen, B. and Lüttgen, G.: Compositional Minimisation of Finite State Systems Using Interface Specifications,Formal Aspects of Computing 8(E):xxx–xxx.
Josko, B.: MCTL — an extension of CTL for modular verification of concurrent systems. InWorkshop on Temporal Logic in Specification, volume 398 ofLNCS, 1987.
Loiseaux, C., Graf, S., Sifakis, J., Bouajjani, A. and Bensalem, S.: Property preserving abstractions for the verification of concurrent systems.Formal Methods in System Design,Vol 6, Iss 1, 1995.
Larsen, K. G., Steffen, B. and Weise, C.: A constraint oriented proof methodology based on modal transition systems. In BRICS Notes 94-6, December 1994.
Larsen, K. G. and Thomsen, B.: Compositional proofs by partial specification of processes.Proc. IEEE Symp. Logic in Computer Science, 1988.
Milner, R.:Communication and Concurrency. Prentice Hall, 1989.
Peled, D.: All from one, one for all: on model checking using representatives. InProceedings of the International Conference on Computer Aided Verification (CAV'93), volume 697 ofLNCS, 1993.
Pnueli, A.: In transition from global to modular temporal reasoning about programs. InLogics and Models for Concurrent Systems, volume 13 ofNATO ASI Series F. Springer Verlag, 1990.
Shurek, G. and Grumberg, O.: The modular framework of computer-aided verification. InWorkshop on Automatic Verification '90, volume 531 ofLNCS, pages 214–223, 1990.
Steffen, B., Margaria, T. and Claßen, A.: Heterogeneous analysis and verification for distributed systems.Software—Concepts and Tools, 17:13–25, 1996.
Vaandrager, F. W.: Some observations on redundancy in a context. In J.C.M. Baeten, editor,Applications of Process Algebra, volume 17 ofCambridge Tracts in Theoretical Computer Science, pages 237–260. Cambridge University Press, 1990.
Valmari, A.: On-the-fly verification with stubborn sets. InProceedings of the International Conference on Computer Aided Verification (CAV'93), volume 697of LNCS, pages 397–408, 1993.
Walker, D. J.: Bisimulation and divergence in CCS.Proc. IEEE Symp. Logic in Computer Science, 1988.
Winskel, G.: Compositional checking of validity on finite state processes. InWorkshop on Theories of Communication, CONCUR, volume 458 ofLNCS, 1990.
Author information
Authors and Affiliations
Additional information
A preliminary version appeared inProceedings of CAV'90 — Second International Workshop on Computer-Aided Verification, Vol. 531Lecture Notes in Computer Science, Springer, pp. 186–196, June 1990.
Electronic supplementary material
Rights and permissions
About this article
Cite this article
Graf, S., Steffen, B. & Lüttgen, G. Compositional minimisation of finite state systems using interface specifications. Formal Aspects of Computing 8, 607–616 (1996). https://doi.org/10.1007/BF01211911
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/BF01211911