Skip to main content
SpringerLink
Log in

Modeling Concurrent Behaviors as Words

  • Conference paper
  • First Online:
Verification and Evaluation of Computer and Communication Systems (VECoS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11847))

  • 214 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Abadi, M., Lamport, L.: Composing specifications. ACM Trans. Program. Lang. Syst. 15(1), 73–132 (1993)

    Article  Google Scholar 

  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. Alur, R., Peled, D.: Undecidability of partial order logics. Inf. Process. Lett. 69(3), 137–143 (1999)

    Article  MathSciNet  Google Scholar 

  4. Arnold, A., Niwinski, D.: Rudiments of \(\mu \)-Calculus. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  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. Cheng, A.: Petri nets, traces, and local model checking. Theor. Comput. Sci. 183(2), 229–251 (1997)

    Article  MathSciNet  Google Scholar 

  7. Courcelle, B., Engelfriet, J.: Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach, 1st edn. Cambridge University Press, Cambridge (2012)

    Book  Google Scholar 

  8. Gastin, P., Kuske, D.: Uniform satisfiability problem for local temporal logics over mazurkiewicz traces. Inf. Comput. 208(7), 797–816 (2010)

    Article  MathSciNet  Google Scholar 

  9. Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)

    Google Scholar 

  10. Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)

    Article  Google Scholar 

  11. Lodaya, K., Weil, P.: Series-parallel languages and the bounded-width property. Theor. Comput. Sci. 237(1), 347–380 (2000)

    Article  MathSciNet  Google Scholar 

  12. Madhusudan, P.: Model-checking trace event structures. In: Logic in Computer Science, 2003, pp. 371–380. IEEE (2003)

    Google Scholar 

  13. Mazurkiewicz, A.: Concurrent program schemes and their interpretations. In: DAIMI Report Series 6(78), July (1977)

    Google Scholar 

  14. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publisher, Boston (1994)

    MATH  Google Scholar 

  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. Mukund, M., Thiagarajan, P.S.: Linear time temporal logics over mazurkiewicz traces. In: Mathematical Foundations of Computer Science, pp. 62–92 (1996)

    Chapter  Google Scholar 

  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_8

    Chapter  Google Scholar 

  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_27

    Chapter  Google Scholar 

  19. Nielsen, M., Plotkin, G., Winskel, G.: Petri nets, event structures and domains, part i. Theor. Comput. Sci. 13(1), 85–108 (1981)

    Article  Google Scholar 

  20. Ramanujam, R.: Locally linear time temporal logic. In: IEEE Symposium on Logic in Computer Science, pp. 118–127 (1996)

    Google Scholar 

  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_24

    Chapter  Google Scholar 

  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_7

    Chapter  Google Scholar 

  23. Weil, P.: Algebraic recognizability of languages. Math. Found. Comput. Sci. 3153, 149–175 (2004)

    MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

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

Author information

Authors and Affiliations

  1. Laboratoire d’Informatique Fondamentale d’Orléans, Université d’Orléans, 45067, Orleans Cedex 2, France

    Yohan Boichut, Jean-Michel Couvreur, Xavier Ferry & Mohamadou Tafsir Sakho

Authors
  1. Yohan Boichut
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-Michel Couvreur
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xavier Ferry
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mohamadou Tafsir Sakho
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jean-Michel Couvreur .

Editor information

Editors and Affiliations

  1. IMDEA Software Institute, Pozuelo de Alarcón, Spain

    Pierre Ganty

  2. Laboratory for Analysis and Architecture, Toulouse, France

    Mohamed Kaâniche

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Boichut, Y., Couvreur, JM., Ferry, X., Sakho, M.T. (2019). Modeling Concurrent Behaviors as Words. In: Ganty, P., Kaâniche, M. (eds) Verification and Evaluation of Computer and Communication Systems. VECoS 2019. Lecture Notes in Computer Science(), vol 11847. Springer, Cham. https://doi.org/10.1007/978-3-030-35092-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-35092-5_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-35091-8

  • Online ISBN: 978-3-030-35092-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation