Abstract
This tutorial is an introduction to compositionality and externally observable behaviour. To make it easier to understand system descriptions, traditional process-algebraic languages have been replaced by state machines represented as annotated directed graphs. Emphasis is on a novel way of treating local variables, and on the Chaos-Free Failures Divergences semantics. Even so, big themes that are not tied to any particular semantics are pointed out where possible. Other semantic models are introduced briefly. Most important verification methods facilitated by compositionality are mentioned with pointers to literature. Mathematical details are given less attention but not left out altogether. Throughout the tutorial, important principles are summarized in framed pieces of text.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Arnold, A.: Finite Transition Systems. Prentice-Hall, Englewood Cliffs (1994)
Bartlett, K.A., Scantlebury, R.A., Wilkinson, P.T.: A Note on Reliable Full-Duplex Transmission over Half-Duplex Links. Communications of the ACM 12(5), 260–261 (1969)
Bolognesi, T., Brinksma, E.: Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems 14(1), 25–59 (1987)
Cleaveland, R., Hennessy, M.: Testing Equivalence as a Bisimulation Equivalence. Formal Aspects of Computing 5(1), 1–20 (1993)
De Nicola, R., Vaandrager, F.: Three Logics for Branching Bisimulation. Journal of the ACM 42(2), 458–487 (1995)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, pp. 995–1072. The MIT Press/Elsevier (1990)
Engelfriet, J.: Determinacy \(\longrightarrow\) (Observation Equivalence = Trace Equivalence). Theoretical Computer Science 36(1), 21–25 (1985)
Fernandez, J.-C.: An Implementation of an Efficient Algorithm for Bisimulation Equivalence. Science of Computer Programming 13(2-3), 219–236 (1989/1990)
Graf, S., Steffen, B., Lüttgen, G.: Compositional Minimisation of Finite State Systems Using Interface Specifications. Formal Aspects of Computing 8(5), 607–616 (1996)
Hansen, H., Valmari, A.: Operational Determinism and Fast Algorithms. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 188–202. Springer, Heidelberg (2006)
Hansen, H., Virtanen, H., Valmari, A.: Merging State-based and Action-based Verification. In: Lilius, J., Balarin, F., Machado, R.J. (ed.) 3rd International Conference on Application of Concurrency to System Design (ACSD 2003), pp. 150–156. IEEE Computer Society (2003)
Helovuo, J., Valmari, A.: Checking for CFFD-Preorder with Tester Processes. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 283–298. Springer, Heidelberg (2000)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall, Englewood Cliffs (1985)
Kaivola, R., Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. In: Cleaveland, R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 207–221. Springer, Heidelberg (1992)
Kanellakis, P.C., Smolka, S.A.: CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Information and Computation 86(1), 43–68 (1990)
Kangas, A., Valmari, A.: Verification with the Undefined: A New Look. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science, vol. 80, pp. 124–139 (2003)
Karsisto, K.: A New Parallel Composition Operator for Verification Tools. Dr.Tech. Thesis, Tampere University of Technology Publications 420, Tampere, Finland (2003)
Madelaine, E., Vergamini, D.: AUTO: A Verification Tool for Distributed Systems Using Reduction of Finite Automata Networks. In: Vuong, S.T. (ed.) Formal Description Techniques II (FORTE 1989), pp. 61–66. North-Holland (1990)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems, vol. I: Specification. Springer (1992)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Puhakka, A.: Weakest Congruences, Fairness and Compositional Process-Algebraic Verification. Dr.Tech. Thesis, Tampere University of Technology Publications 468, Tampere, Finland (2004)
Puhakka, A., Valmari, A.: Liveness and Fairness in Process-Algebraic Verification. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 202–217. Springer, Heidelberg (2001)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)
Roscoe, A.W.: Seeing Beyond Divergence. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) CSP25. LNCS, vol. 3525, pp. 15–35. Springer, Heidelberg (2005)
Roscoe, A.W.: Understanding Concurrent Systems. Springer (2010)
Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through Determinism. Journal of Computer Security 4(1), 27–54 (1996)
Sabnani, K.K., Lapone, A.M., Uyar, M.Ü.: An Algorithmic Procedure for Checking Safety Properties of Protocols. IEEE Transactions on Communications 37(9), 940–948 (1989)
Valmari, A.: The Weakest Deadlock-Preserving Congruence. Information Processing Letters 53(6), 341–346 (1995)
Valmari, A.: Failure-Based Equivalences Are Faster Than Many Believe. In: Desel, J. (ed.) Structures in Concurrency Theory 1995. Workshops in Computing, pp. 326–340. Springer (1995)
Valmari, A.: Compositionality in State Space Verification Methods. In: Billington, J., Reisig, W. (eds.) ICATPN 1996. LNCS, vol. 1091, pp. 29–56. Springer, Heidelberg (1996)
Valmari, A.: Stubborn Set Methods for Process Algebras. In: Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.) Partial Order Methods in Verification: DIMACS Workshop. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231. American Mathematical Society (1997)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491, pp. 429–528. Springer, Heidelberg (1998)
Valmari, A.: A Chaos-Free Failures Divergences Semantics with Applications to Verification. In: Davies, J., Roscoe, B., Woodcock, J. (eds.) Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare, pp. 365–382. Palgrave (2000)
Valmari, A.: Composition and Abstraction. In: Cassez, F., Jard, C., Rozoy, B., Ryan, M.D. (eds.) MOVEP 2000. LNCS, vol. 2067, pp. 58–98. Springer, Heidelberg (2001)
Valmari, A.: Simple Bisimilarity Minimization in O(m logn) Time. Fundamenta Informaticae 105(3), 319–339 (2010)
Valmari, A., Kervinen, A.: Alphabet-Based Synchronisation is Exponentially Cheaper. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 161–176. Springer, Heidelberg (2002)
Valmari, A., Kokkarinen, I.: Unbounded Verification Results by Finite-State Compositional Techniques: 10any States and Beyond. In: Lavagno, L., Reisig, W. (eds.) International Conference on Application of Concurrency to System Design (ACSD 1998), pp. 75–85. IEEE Computer Society (1998)
Valmari, A., Setälä, M.: Visual Verification of Safety and Liveness. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 228–247. Springer, Heidelberg (1996)
Valmari, A., Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. In: Jonsson, B., Parrow, J., Pehrson, B. (eds.) Protocol Specification, Testing and Verification XI, pp. 3–18. North-Holland (1991)
Valmari, A., Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. Formal Aspects of Computing 7(4), 440–468 (1995)
van Glabbeek, R.J., Weijland, W.P.: Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3), 555–600 (1996)
Voorhoeve, M., Mauw, S.: Impossible Futures and Determinism. Information Processing Letters 80(1), 51–58 (2001)
Wolper, P., Lovinfosse, V.: Verifying Properties of Large Sets of Processes with Network Invariants. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 68–80. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A. (2013). External Behaviour of Systems of State Machines with Variables. In: Jensen, K., van der Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds) Transactions on Petri Nets and Other Models of Concurrency VII. Lecture Notes in Computer Science, vol 7480. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38143-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-38143-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38142-3
Online ISBN: 978-3-642-38143-0
eBook Packages: Computer ScienceComputer Science (R0)