nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Language Inclusion for Finite Prime Event Structures

verfasst von : Andreas Fellner, Thorsten Tarrach, Georg Weissenbacher

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a language of sequences of labels produced by the represented system. We study the problem of deciding inclusion and membership for languages encoded by finite prime event structures and provide complexity results for both problems. We provide a family of examples where prime event structures are exponentially more succinct than formalisms that do not take concurrency into account. We provide a decision algorithm for language inclusion that exploits this succinctness. Furthermore, we provide an implementation of the algorithm and an evaluation on a series of benchmarks. Finally, we demonstrate how our results can be applied to mutation-based test case generation.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Generalized Property-Directed Reachability for Hybrid Systems

Nächstes Kapitel Promptness and Bounded Fairness in Concurrent and Parameterized Systems

Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When simulation meets antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-12002-2_14CrossRefMATH

Bertoni, A., Mauri, G., Sabadini, N.: Equivalence and membership problems for regular trace languages. In: Nielsen, M., Schmidt, E.M. (eds.) ICALP 1982. LNCS, vol. 140, pp. 61–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0012757CrossRefMATH

Bertoni, A., Mauri, G., Sabadini, N.: Membership problems for regular and context-free trace languages. Inf. Comput. 82(2), 135–150 (1989)MathSciNetCrossRef

Bouajjani, A., Enea, C., Lahiri, S.K.: Abstract semantic diffing of evolving concurrent programs. In: Ranzato, F. (ed.) Proceedings of the Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, 30 August–1 September 2017, LNCS, vol. 10422, pp. 46–65. Springer (2017). https://doi.org/10.1007/978-3-319-66706-5_3CrossRef

Boudol, G.: Flow event structures and flow nets. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 62–95. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_4CrossRef

Černý, P., et al.: From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods Syst. Des. 50(2), 97–139 (2017)CrossRef

Diekert, V., Métivier, Y.: Partial commutation and traces. In: Rozenberg, G., Salomaa, A. (eds.) Handbook of Formal Languages, pp. 457–533. Springer, Heidelberg (1997). https://doi.org/10.1007/978-3-642-59126-6_8CrossRef

Dietsch, D., Jakobs, M.C.: VMCAI 2020 virtual machine, November 2019. https://doi.org/10.5281/zenodo.3533104

Clarke, J.E.M., Grumberg, O., Kroening, D., Peled, D., Veith, H.: Model Checking. 2nd edn. MIT Press (2018)

10.

Esparza, J.: Decidability and complexity of Petri net problems — an introduction. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 374–428. Springer, Heidelberg (1998). https://doi.org/10.1007/3-540-65306-6_20CrossRefMATH

11.

Esparza, J., Nielsen, M.: Decidability issues for Petri nets - a survey. Bull. EATCS 52, 244–262 (1994)MATH

12.

Fatès, N.: A guided tour of asynchronous cellular automata. In: Kari, J., Kutrib, M., Malcher, A. (eds.) AUTOMATA 2013. LNCS, vol. 8155, pp. 15–30. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40867-0_2CrossRefMATH

13.

Fellner, A., Krenn, W., Schlick, R., Tarrach, T., Weissenbacher, G.: Model-based, mutation-driven test-case generation via heuristic-guided branching search. ACM Trans. Embed. Comput. Syst. 18(1), 4:1–4:28 (2019)CrossRef

14.

Fellner, A., Tarrach, T., Weissenbacher, G.: Language inclusion for finite prime event structures (2019). https://arxiv.org/abs/1911.06355

15.

Fellner, A., Tarrach, T., Weissenbacher, G.: Language Inclusion for Finite Prime Event Structures. Artifact (2019). https://doi.org/10.5281/zenodo.3514619

16.

Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297–316 (1976)MathSciNetCrossRef

17.

Gaubert, S., Giua, A.: Petri net languages and infinite subsets of Nm. J. Comput. Syst. Sci. 59(3), 373–391 (1999). https://doi.org/10.1006/jcss.1999.1634CrossRefMATH

18.

van Glabbeek, R., Goltz, U.: Refinement of actions in causality based models. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1989. LNCS, vol. 430, pp. 267–300. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52559-9_68CrossRef

19.

van Glabbeek, R.J., Plotkin, G.D.: Configuration structures, event structures and Petri nets. Theor. Comput. Sci. 410(41), 4111–4159 (2009)MathSciNetCrossRef

20.

Godefroid, P.: Partial-order methods for the verification of concurrent systems (1996)

21.

Grabowski, J.: The unsolvability of some Petri net language problems. Inf. Process. Lett. 9(2), 60–63 (1979). https://doi.org/10.1016/0020-0190(79)90128-5MathSciNetCrossRefMATH

22.

Hack, M.: Decidability questions for Petri Nets. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, USA (1976). http://hdl.handle.net/1721.1/27441

23.

Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. 3rd edn. Pearson (2013)

24.

Jancar, P.: Nonprimitive recursive complexity and undecidability for Petri net equivalences. Theor. Comput. Sci. 256(1–2), 23–30 (2001). https://doi.org/10.1016/S0304-3975(00)00100-6MathSciNetCrossRefMATH

25.

Jones, N.D., Landweber, L.H., Lien, Y.E.: Complexity of some problems in Petri nets. Theor. Comput. Sci. 4(3), 277–299 (1977). https://doi.org/10.1016/0304-3975(77)90014-7MathSciNetCrossRefMATH

26.

Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R.E., Thatcher, J.W., Bohlinger, J.D. (eds.) Complexity of Computer Computations. The IBM Research Symposia Series, pp. 85–103. Springer, Boston (1972). https://doi.org/10.1007/978-1-4684-2001-2_9CrossRef

27.

Ko, K.I., Lin, C.L.: On the complexity of min-max optimization problems and their approximation. In: Du, D.Z., Pardalos, P.M. (eds.) Minimax and Applications. Nonconvex Optimization and Its Applications, vol. 4, pp. 219–239. Springer, Boston (1995). https://doi.org/10.1007/978-1-4613-3557-3_15CrossRef

28.

Lamport, L., et al.: Paxos made simple. ACM SIGACT News 32(4), 18–25 (2001)

29.

Madhusudan, P.: Model-checking trace event structures. In: Proceedings of the 18th IEEE Symposium on Logic in Computer Science (LICS 2003), Ottawa, Canada, 22–25 June 2003, pp. 371–380. IEEE Computer Society (2003). https://doi.org/10.1109/LICS.2003.1210077

30.

Mayr, R., Clemente, L.: Advanced automata minimization. In: ACM SIGPLAN Notices, vol. 48, pp. 63–74. ACM (2013)

31.

Mazurkiewicz, A.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 255, pp. 278–324. Springer, Heidelberg (1987). https://doi.org/10.1007/3-540-17906-2_30CrossRef

32.

Mazurkiewicz, A.: Introduction to trace theory. In: The Book of Traces, pp. 3–41 (1995)CrossRef

33.

Meyer, A.R., Stockmeyer, L.J.: The equivalence problem for regular expressions with squaring requires exponential space. In: SWAT (FOCS), pp. 125–129 (1972)

34.

Nguyen, H.T.T., Rodríguez, C., Sousa, M., Coti, C., Petrucci, L.: Quasi-optimal partial order reduction. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 354–371. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96142-2_22CrossRef

35.

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

36.

Penczek, W.: Model-checking for a subclass of event structures. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 145–164. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0035386CrossRef

37.

Peterson, J.: Petri Net Theory and the Modeling of Systems. Independently Published (2019). https://books.google.at/books?id=IthLyAEACAAJ

38.

Rodríguez, C., Sousa, M., Sharma, S., Kroening, D.: Unfolding-based partial order reduction. In: 26th International Conference on Concurrency Theory (CONCUR 2015), pp. 456–469 (2015)

39.

Stearns, R.E., Hunt III, H.B.: On the equivalence and containment problems for unambiguous regular expressions, regular grammars and finite automata. SIAM J. Comput. 14(3), 598–611 (1985)MathSciNetCrossRef

40.

Valk, R., Vidal-Naquet, G.: Petri nets and regular languages. J. Comput. Syst. Sci. 23(3), 299–325 (1981). https://doi.org/10.1016/0022-0000(81)90067-2MathSciNetCrossRefMATH

41.

Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53863-1_36CrossRef

42.

Van Glabbeek, R., Goltz, U.: Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37(4–5), 229–327 (2001)MathSciNetCrossRef

43.

Winskel, G.: An introduction to event structures. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1988. LNCS, vol. 354, pp. 364–397. Springer, Heidelberg (1989). https://doi.org/10.1007/BFb0013026CrossRef

44.

Winskel, G.: Event structures, stable families and concurrent games (2016)

45.

Winskel, G., Nielsen, M.: Handbook of logic in computer science. In: Models for Concurrency, vol. 4, pp. 1–148. Oxford University Press Inc., New York (1995). http://dl.acm.org/citation.cfm?id=218623.218630

46.

Wrathall, C.: Complete sets and the polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 23–33 (1976)MathSciNetCrossRef

47.

Zielonka, W.: Notes on finite asynchronous automata. RAIRO-Theor. Inf. Appl. 21(2), 99–135 (1987)MathSciNetCrossRef

Titel: Language Inclusion for Finite Prime Event Structures
verfasst von: Andreas Fellner
Thorsten Tarrach
Georg Weissenbacher
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

Electronic ISBN: 978-3-030-39322-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39322-9_15

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"