Advertisement

Modeling Concurrent Behaviors as Words

  • Yohan Boichut
  • Jean-Michel CouvreurEmail author
  • Xavier Ferry
  • Mohamadou Tafsir Sakho
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11847)

Abstract

Performing formal verification of concurrent systems involves partial order logics (here MSO with partial orders) for the specification of properties or of the concurrent system itself. A common structure for the verification of concurrent systems is so-called pomset. A pomset is a multiset of partially ordered events. The partial order relation describes causal dependencies of events. We propose a new word based model, namely Pre-Post-Pomset, making the exploration of pomsets space possible. In this paper, our new model stands to be a general model in the sense that some classical models used in the specification of concurrent systems (Synchronized product of systems, Mazurkiewicz traces or parallel series) can be specified within. Besides its general aspect, our model offers decidability results on the verification problem according to an MSO formula on pomsets.

Keywords

Partial order Pomset Specification Models Concurrent systems 

Notes

Acknowledgments

We are immensely grateful to Anthony Perez for his comments on an earlier version of the manuscript.

References

  1. 1.
    Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Peled, D.A., Penczek, W.: Model-checking of causality properties. In: IEEE Symposium on Logic in Computer Science, pp. 90–100 (1995)Google Scholar
  3. 3.
    Alur, R., Peled, D.: Undecidability of partial order logics. Inf. Process. Lett. 69(3), 137–143 (1999)MathSciNetCrossRefGoogle Scholar
  4. 4.
    Arnold, A., Niwinski, D.: Rudiments of \(\mu \)-Calculus. Elsevier, Amsterdam (2001)zbMATHGoogle Scholar
  5. 5.
    Büchi, J.R.: On a decision method in restricted second order arithmetic. In: International Congress on Logic, Methodology and Philosophy of Science, pp. 1–11. Stanford University Press (1962)Google Scholar
  6. 6.
    Cheng, A.: Petri nets, traces, and local model checking. Theor. Comput. Sci. 183(2), 229–251 (1997)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, 1st edn. Cambridge University Press, Cambridge (2012)CrossRefGoogle Scholar
  8. 8.
    Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over mazurkiewicz traces. Inf. Comput. 208(7), 797–816 (2010)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)Google Scholar
  10. 10.
    Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRefGoogle Scholar
  11. 11.
    Lodaya, K., Weil, P.: Series-parallel languages and the bounded-width property. Theor. Comput. Sci. 237(1), 347–380 (2000)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Madhusudan, P.: Model-checking trace event structures. In: Logic in Computer Science, 2003, pp. 371–380. IEEE (2003)Google Scholar
  13. 13.
    Mazurkiewicz, A.: Concurrent program schemes and their interpretations. In: DAIMI Report Series 6(78), July (1977)Google Scholar
  14. 14.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Boston (1994)zbMATHGoogle Scholar
  15. 15.
    Meenakshi, B., Ramanujam, R.: Reasoning about layered message passing systems. In: Verification, Model Checking, and Abstract Interpretation, pp. 268–282 (2003)Google Scholar
  16. 16.
    Mukund, M., Thiagarajan, P.S.: Linear time temporal logics over mazurkiewicz traces. In: Mathematical Foundations of Computer Science, pp. 62–92 (1996)CrossRefGoogle Scholar
  17. 17.
    Muscholl, A., Peled, D.: Message sequence graphs and decision problems on mazurkiewicz traces. In: Kutylowski, M., Pacholski, L., Wierzbicki, T. (eds.) MFCS 1999. LNCS, vol. 1672, pp. 81–91. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48340-3_8CrossRefGoogle Scholar
  18. 18.
    Niebert, P., Huhn, M., Zennou, S., Lugiez, D.: Local first search — a new paradigm for partial order reductions. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 396–410. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-44685-0_27CrossRefGoogle Scholar
  19. 19.
    Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part i. Theor. Comput. Sci. 13(1), 85–108 (1981)CrossRefGoogle Scholar
  20. 20.
    Ramanujam, R.: Locally linear time temporal logic. In: IEEE Symposium on Logic in Computer Science, pp. 118–127 (1996)Google Scholar
  21. 21.
    Thiagarajan, P.S., Henriksen, J.G.: Distributed versions of linear time temporal logic: a trace perspective. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 643–681. Springer, Heidelberg (1998).  https://doi.org/10.1007/3-540-65306-6_24CrossRefGoogle Scholar
  22. 22.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 389–455. Springer, Heidelberg (1997).  https://doi.org/10.1007/978-3-642-59126-6_7CrossRefGoogle Scholar
  23. 23.
    Weil, P.: Algebraic recognizability of languages. Math. Found. Comput. Sci. 3153, 149–175 (2004)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Yohan Boichut
    • 1
  • Jean-Michel Couvreur
    • 1
    Email author
  • Xavier Ferry
    • 1
  • Mohamadou Tafsir Sakho
    • 1
  1. 1.Laboratoire d’Informatique Fondamentale d’OrléansUniversité d’OrléansOrleans Cedex 2France

Personalised recommendations