nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

From the Archives of the Formal Methods and Tools Lab

Axiomatising and Contextualising ACTL

verfasst von : Stefania Gnesi, Maurice H. ter Beek

Erschienen in: Models, Languages, and Tools for Concurrent and Distributed Programming

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 present a sound and complete axiomatisation of ACTL, an action-based version of the well-known branching-time temporal logic CTL, and place it into a historical context. ACTL was originally introduced by Rocco De Nicola together with Frits Vaandrager 30 years ago, and it has played a major role in shaping the activity of our Formal Methods and Tools Lab from the nineties to this very day.

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 Different Glasses to Look into the Three Cs: Component, Connector, Coordination

Nächstes Kapitel Featherweight Scribble

A preliminary version of the axiom system was presented in [40]; here we provide a more succinct set of axioms, based on the fact that the eventually and always operators F and G can be expressed in terms of the Until operator U, cf. Sect. 3.

Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Theoretical Computer Science, vol. 18. Cambridge University Press, Cambridge (1990). https://doi.org/10.1017/CBO9780511624193CrossRefMATH

Baeten, J.C.M., Basten, T., Reniers, M.A.: Process Algebra: Equational Theories of Communicating Processes. Cambridge Tracts in Theoretical Computer Science, vol. 50. Cambridge University Press, Cambridge (2010). https://doi.org/10.1017/CBO9781139195003CrossRefMATH

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: An action/state-based model-checking approach for the analysis of communication protocols for service-oriented applications. In: Leue, S., Merino, P. (eds.) FMICS 2007. LNCS, vol. 4916, pp. 133–148. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-79707-4_11CrossRef

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: A state/event-based model-checking approach for the analysis of abstract system properties. Sci. Comput. Program. 76(2), 119–135 (2011). https://doi.org/10.1016/j.scico.2010.07.002CrossRefMATH

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: Using FMC for family-based analysis of software product lines. In: Proceedings of the 19th International Software Product Line Conference (SPLC 2015), pp. 432–439. ACM (2015). https://doi.org/10.1145/2791060.2791118

ter Beek, M.H., Fantechi, A., Gnesi, S., Mazzanti, F.: States and events in KandISTI: a retrospective. In: Margaria, T., Graf, S., Larsen, K.G. (eds.) Models, Mindsets, Meta: The What, the How, and the Why Not? LNCS, vol. 11200. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-22348-9_9

ter Beek, M.H., Gnesi, S., Mazzanti, F.: From EU projects to a family of model checkers. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 312–328. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15545-6_20CrossRef

ter Beek, M.H., Mazzanti, F., Gnesi, S.: CMC-UMC: a framework for the verification of abstract service-oriented properties. In: Proceedings of the 24th Annual ACM Symposium on Applied Computing (SAC 2009), pp. 2111–2117. ACM (2009). https://doi.org/10.1145/1529282.1529751

ter Beek, M.H., Mazzanti, F., Sulova, A.: VMC: a tool for product variability analysis. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 450–454. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_36CrossRef

10.

ter Beek, M.H., Mazzanti, F.: VMC: recent advances and challenges ahead. In: Proceedings of the 18th International Software Product Line Conference (SPLC 2014), pp. 70–77. ACM (2014). https://doi.org/10.1145/2647908.2655969

11.

Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. In: Proceedings of the 8th Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages (POPL 1981), pp. 164–176. ACM (1981). https://doi.org/10.1145/567532.567551

12.

Ben-Ari, M., Pnueli, A., Manna, Z.: The temporal logic of branching time. Acta Inform. 20(3), 207–226 (1983). https://doi.org/10.1007/BF01257083MathSciNetCrossRefMATH

13.

Bernardeschi, C., Fantechi, A., Gnesi, S., Larosa, S., Mongardi, G., Romano, D.: A formal verification environment for railway signaling system design. Formal Methods Syst. Des. 12(2), 139–161 (1998). https://doi.org/10.1023/A:1008645826258CrossRef

14.

Bouali, A., Gnesi, S., Larosa, S.: JACK: Just Another Concurrency Kit - the integration project. Bull. EATCS 54, 207–223 (1994)MATH

15.

Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982). https://doi.org/10.1007/BFb0025774CrossRef

16.

Clarke, E.M., Emerson, E.A.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241–266 (1982). https://doi.org/10.1016/0167-6423(83)90017-5CrossRefMATH

17.

Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications: a practical approach. In: Proceedings of the 10th Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages (POPL 1983), pp. 117–126. ACM (1983). https://doi.org/10.1145/567067.567080

18.

Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986). https://doi.org/10.1145/5397.5399CrossRefMATH

19.

De Nicola, R., Fantechi, A., Gnesi, S., Larosa, S., Ristori, G.: Verifying hardware components with JACK. In: Camurati, P.E., Eveking, H. (eds.) CHARME 1995. LNCS, vol. 987, pp. 246–260. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60385-9_15CrossRef

20.

De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action based framework for verifying logical and behavioural properties of concurrent systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 37–47. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55179-4_5CrossRef

21.

De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action-based framework for verifying logical and behavioural properties of concurrent systems. Comput. Netw. ISDN Syst. 25(7), 761–778 (1993). https://doi.org/10.1016/0169-7552(93)90047-8CrossRefMATH

22.

De Nicola, R., Inverardi, P., Nesi, M.: Using the axiomatic presentation of behavioural equivalences for manipulating CCS specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 54–67. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-52148-8_5CrossRef

23.

De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990). https://doi.org/10.1007/3-540-53479-2_17CrossRef

24.

De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation (extended abstract). In: Proceedings of the 5th Annual Symposium on Logic in Computer Science (LICS 1990), pp. 118–129. IEEE (1990). https://doi.org/10.1109/LICS.1990.113739

25.

De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995). https://doi.org/10.1145/201019.201032MathSciNetCrossRefMATH

26.

Emerson, E.A.: Temporal and modal logic. In: Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B, pp. 995–1072. Elsevier (1990). https://doi.org/10.1016/B978-0-444-88074-1.50021-4MATH

27.

Emerson E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time (preliminary report). In: Proceedings of the 10th Annual ACM SIGACT/SIGPLAN Symposium on Principles of Programming Languages (POPL 1983), pp. 127–140. ACM (1983). https://doi.org/10.1145/567067.567081

28.

Emerson, E.A., Halpern, J.Y.: “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151–178 (1986). https://doi.org/10.1145/4904.4999MathSciNetCrossRefMATH

29.

Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. In: Proceedings of the 14th Annual ACM Symposium on Theory of Computing (STOC 1982), pp. 169–180. ACM (1982). https://doi.org/10.1145/800070.802190

30.

Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1–24 (1985). https://doi.org/10.1016/0022-0000(85)90001-7MathSciNetCrossRefMATH

31.

Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs (extended abstract). In: Proceedings of the 29th Annual Symposium on Foundations of Computer Science (FOCS 1988), pp. 328–337. IEEE (1988). https://doi.org/10.1109/SFCS.1988.21949

32.

Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132–158 (1999). https://doi.org/10.1137/S0097539793304741MathSciNetCrossRefMATH

33.

Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mu-calculus (extended abstract). In: Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986), pp. 267–278. IEEE (1986)

34.

Emerson, E.A., Sistla, A.P.: Deciding full branching time logic. Inf. Control 61(3), 175–201 (1984). https://doi.org/10.1016/S0019-9958(84)80047-9MathSciNetCrossRefMATH

35.

Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A logical verification methodology for service-oriented computing. ACM Trans. Softw. Eng. Methodol. 21(3), 161–1646 (2012). https://doi.org/10.1145/2211616.2211619CrossRef

36.

Fantechi, A., Gnesi, S., Mazzanti, F., Pugliese, R., Tronci, E.: A symbolic model checker for ACTL. In: Hutter, D., Stephan, W., Traverso, P., Ullmann, M. (eds.) FM-Trends 1998. LNCS, vol. 1641, pp. 228–242. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48257-1_14CrossRef

37.

Fantechi, A., Gnesi, S., Ristori, G.: Model checking for action-based logics. Formal Methods Syst. Des. 4(2), 187–203 (1994). https://doi.org/10.1007/BF01384084CrossRefMATH

38.

Fantechi, A., Gnesi, S., Semini, L.: Formal description and validation for an integrity policy supporting multiple levels of criticality. In: Dependable Computing and Fault-Tolerant Systems: Proceedings of the 7th IFIP International Conference on Dependable Computing for Critical Applications (DCCA-7), vol. 12, pp. 129–146. IEEE (1999). https://doi.org/10.1109/DCFTS.1999.814293

39.

Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979). https://doi.org/10.1016/0022-0000(79)90046-1MathSciNetCrossRefMATH

40.

Gnesi, S., Larosa, S.: A sound and complete axiom system for the logic ACTL. In: Proceedings of the 5th Italian Conference on Theoretical Computer Science (ICTCS 1995), pp. 343–358. World Scientific (1996). https://doi.org/10.1142/9789814531184

41.

Gnesi, S., Mazzanti, F.: On the fly verification of networks of automata. In: Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA 1999), pp. 1040–1046. CSREA Press (1999)

42.

Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985). https://doi.org/10.1145/2455.2460MathSciNetCrossRefMATH

43.

Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Englewood Cliffs (1985)MATH

44.

Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)MATH

45.

Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44585-4_2CrossRef

46.

Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45294-X_25CrossRef

47.

Pnueli, A.: Linear and branching structures in the semantics and logics of reactive systems. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 15–32. Springer, Heidelberg (1985). https://doi.org/10.1007/BFb0015727CrossRef

48.

Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol. 137, pp. 337–351. Springer, Heidelberg (1982). https://doi.org/10.1007/3-540-11494-7_22CrossRef

49.

Ray, S.: Scalable Techniques for Formal Verification. Springer, Heidelberg (2010). https://doi.org/10.1007/978-1-4419-5998-0CrossRefMATH

50.

Reynolds, M.: An axiomatization of full computation tree logic. J. Symb. Log. 66(3), 1011–1057 (2001). https://doi.org/10.2307/2695091MathSciNetCrossRefMATH

51.

Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs (1997)

52.

Stirling, C.: An introduction to modal and temporal logics for CCS. In: Yonezawa, A., Ito, T. (eds.) CONCURRENCY 1989. LNCS, vol. 491, pp. 1–20. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53932-8_41CrossRef

53.

Stirling, C.: Modal and temporal logics. In: Handbook of Logic in Computer Science. Background: Computational Structures, vol. 2, pp. 477–563. Oxford University Press (1993)

Titel: From the Archives of the Formal Methods and Tools Lab
verfasst von: Stefania Gnesi
Maurice H. ter Beek
Verlag: Springer International Publishing
Buch: Models, Languages, and Tools for Concurrent and Distributed Programming
Print ISBN: 978-3-030-21484-5

Electronic ISBN: 978-3-030-21485-2

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-21485-2_13

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"