From Box Algebra to Interval Temporal Logic

• Autorzy: Klaudel Hanna , Koutny Maciej , Duan Zhenhua , Moszkowski Ben

Identyfikatory

DOI

10.3233/FI-2019-1820

• Języki publikacji: EN

Abstrakty

EN

In this paper, we further develop a recently introduced semantic link between temporal logics and Petri nets. We focus on two specific formalisms, Interval Temporal Logic (ITL) and Box Algebra (BA), which are closely related by their compositional approach to constructing system descriptions. The overall goal of our investigation is to translate Petri nets into behaviourally equivalent logical formulas. As a result, the analysis of system properties can be carried out using either of the two formalisms, exploiting their respective strengths and powerful tool support. The contribution of this paper is twofold. First, we extend the existing translation from BA to ITL, by removing restrictions concerning the way control flow of concurrent system is modelled, and by allowing a fully general synchronisation operator. Second, we strengthen the notion of equivalence between a Petri net and the corresponding logical formula by proving such an equivalence at the level of transition-based executions of Petri nets rather than just by looking at their labels. We also show that the complexity of the proposed translation compares favourably with the complexity of the translation from BA expressions to Petri nets.

Słowa kluczowe

EN

interval temporal logic; Petri nets; box algebra; composition; semantics; general synchronisation; step sequence; equivalence

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 167, nr 4
• Strony: 323--354
• Opis fizyczny: Bibliogr. 44 poz., rys., tab.

Twórcy

autor

Klaudel Hanna

• IBISC, University of Evry, Université Paris-Saclay 91025, Evry, France

autor

Koutny Maciej

• School of Computing, Newcastle University, Newcastle upon Tyne, NE4 5TG, United Kingdom

autor

Duan Zhenhua

• ICTT and ISN Laboratory, Xidian University, Xi’an, 710071, P.R. China

autor

Moszkowski Ben

• School of Computing, Newcastle University, Newcastle upon Tyne, NE4 5TG, United Kingdom

Bibliografia

• [1] Goranko V, Montanari A, Sciavicco G. A Road Map of Interval Temporal Logics and Duration Calculi. Journal of Applied Non-Classical Logics, 2004. 14(1-2):9-54. doi:10.3166/jancl.14.9-54.
• [2] Emerson EA. Temporal and Modal Logic. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 995-1072. MIT Press Cambridge, 1990. ISBN:0-444-88074-7.
• [3] Manna Z, Pnueli A. Verification of Concurrent Programs: Temporal Proof Principles. In: Kozen D (ed.), Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981, volume 131 of Lecture Notes in Computer Science. Springer. ISBN 3-540-11212-X, 1981 pp. 200-252. doi:10.1007/BFb0025785.
• [4] Moszkowski BC, Guelev DP, Leucker M. Guest editors’ preface to special issue on interval temporal logics. Ann. Math. Artif. Intell., 2014. 71(1-3):1-9. doi:10.1007/s10472-014-9417-7.
• [5] Desel J, Juhás G. ”What Is a Petri Net?”. In: Ehrig H, Juhás G, Padberg J, Rozenberg G (eds.), Unifying Petri Nets, Advances in Petri Nets, volume 2128 of Lecture Notes in Computer Science. Springer. ISBN 3-540-43067-9, 2001 pp. 1-25. doi:10.1007/3-540-45541-8_1.
• [6] Peterka G, Murata T. Proof Procedure and Answer Extraction in Petri Net Model of Logic Programs. IEEE Trans. Software Eng., 1989. 15(2):209-217. doi:10.1109/32.21746.
• [7] Suárez MS, Teruel E, Colom JM. Linear Algebraic and Linear Programming Techniques for the Analysis of Place or Transition Net Systems. In: Reisig W, Rozenberg G (eds.), Lectures on Petri Nets I: Basic Models, Advances in Petri Nets, the volumes are based on the Advanced Course on Petri Nets, held in Dagstuhl, September 1996, volume 1491 of Lecture Notes in Computer Science. Springer. ISBN 3-540-65306-6, 1996 pp. 309-373. doi:10.1007/3-540-65306-6_19.
• [8] McMillan KL. A Technique of State Space Search Based on Unfolding. Formal Methods in System Design, 1995. 6(1):45-65. doi:10.1007/BF01384314.
• [9] Valmari A. Stubborn sets for reduced state space generation. In: Rozenberg G (ed.), Advances in Petri Nets 1990 [10th International Conference on Applications and Theory of Petri Nets, Bonn, Germany, June 1989, Proceedings], volume 483 of Lecture Notes in Computer Science. Springer. ISBN 3-540-53863-1, 1989 pp. 491-515. doi:10.1007/3-540-53863-1_36.
• [10] Duan Z, Klaudel H, Koutny M. ITL semantics of composite Petri nets. J. Log. Algebr. Program., 2013. 82(2):95-110. doi:10.1016/j.jlap.2012.12.001.
• [11] Moszkowski BC. Compositional reasoning about projected and infinite time. In: 1st IEEE International Conference on Engineering of Complex Computer Systems (ICECCS ’95), November 6-10, 1995, Fort Lauderdale, Florida, USA. IEEE Computer Society. ISBN 0-8186-7123-8, 1995 pp. 238-245. doi:10.1109/ICECCS.1995.479336.
• [12] and Zohar Manna. Reasoning in Interval Temporal Logic. In: Clarke EM, Kozen D (eds.), Logics of Programs, Workshop, Carnegie Mellon University, Pittsburgh, PA, USA, June 6-8, 1983, Proceedings, volume 164 of Lecture Notes in Computer Science. Springer. ISBN 3-540-12896-4, 1983 pp. 371-382. doi:10.1007/3-540-12896-4_374.
• [13] Best E, Devillers R, Koutny M. Petri Net Algebra. Monographs in Theoretical Computer Science. Springer, 2001.
• [14] Best E, Devillers RR, Hall JG. The box calculus: a new causal algebra with multi-label communication. In: Rozenberg G (ed.), Advances in Petri Nets 1992, The DEMON Project, volume 609 of Lecture Notes in Computer Science, pp. 21-69. Springer. ISBN 3-540-55610-9, 1992. doi:10.1007/3-540-55610-9_167.
• [15] Milner R. A Calculus of Communicating Systems. Springer, 1980.
• [16] CARHoare. Communicating Sequential Processes. Prentice-Hall, 1985. ISBN-13:978-0131532717, 10:0131532715.
• [17] Best E, Fraczak W, Hopkins RP, Klaudel H, Pelz E. M-Nets: An Algebra of High-Level Petri Nets, with an Application to the Semantics of Concurrent Programming Languages. Acta Inf., 1998. 35(10):813-857. doi:10.1007/s002360050144.
• [18] Macià H, Ruiz VV, Cuartero F, de Frutos-Escrig D. A congruence relation for sPBC. Formal Methods in System Design, 2008. 32(2):85-128. doi:10.1007/s10703-007-0045-2.
• [19] Goranko V, Montanari A. Foreword to Special Issue on Interval Temporal Logics and Duration Calculi. Journal of Applied Non-Classical Logics, 2004. 14(1-2):7-8.
• [20] Bäumler S, Schellhorn G, Tofan B, Reif W. Proving linearizability with temporal logic. Formal Asp. Comput., 2011. 23(1):91-112. doi:10.1007/s00165-009-0130-y.
• [21] Halpern JY, Shoham Y. A Propositional Modal Logic of Time Intervals. J. ACM, 1991. 38(4):935-962. doi:10.1145/115234.115351.
• [22] Venema Y. A Modal Logic for Chopping Intervals. J. Log. Comput., 1991. 1(4):453-476. doi:10.1093/logcom/1.4.453.
• [23] Allen JF. Maintaining Knowledge about Temporal Intervals. Commun. ACM, 1983. 26(11):832-843. doi:10.1145/182.358434.
• [24] Bozzelli L, Molinari A, Montanari A, Peron A, Sala P. Interval vs. Point Temporal Logic Model Checking: An Expressiveness Comparison. ACM Trans. Comput. Log., 2019. 20(1):4:1-4:31. doi:10.1145/3281028.
• [25] Lomuscio A, Michaliszyn J. An Epistemic Halpern-Shoham Logic. In: Rossi F (ed.), IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013. IJCAI/AAAI. ISBN 978-1-57735-633-2, 2013 pp. 1010-1016. URL http://www.aaai.org/ocs/index.php/IJCAI/IJCAI13/paper/view/6632.
• [26] Lomuscio AR, Michaliszyn J. Decidability of model checking multi-agent systems against a class of EHS specifications. In: Schaub T, Friedrich G, O’Sullivan B (eds.), ECAI 2014 - 21st European Conference on Artificial Intelligence, 18-22 August 2014, Prague, Czech Republic-Including Prestigious Applications of Intelligent Systems (PAIS 2014), volume 263 of Frontiers in Artificial Intelligence and Applications. IOS Press. ISBN 978-1-61499-418-3, 2014 pp. 543-548. doi:10.3233/978-1-61499-419-0-543.
• [27] Montanari A, Murano A, Perelli G, Peron A. Checking Interval Properties of Computations. In: Cesta A, Combi C, Laroussinie F (eds.), 21st International Symposium on Temporal Representation and Reasoning, TIME 2014, Verona, Italy, September 8-10, 2014. IEEE Computer Society. ISBN 978-1-4799-4228-2, 2014 pp. 59-68. doi:10.1109/TIME.2014.24.
• [28] Molinari A, Montanari A, Murano A, Perelli G, Peron A. Checking interval properties of computations. Acta Inf., 2016. 53(6-8):587-619. doi:10.1007/s00236-015-0250-1.
• [29] http://www.antonio-cau.co.uk/ITL/.
• [30] Moszkowski BC. Executing Temporal Logic Programs. Cambridge University Press, 1986.
• [31] IEEE: Standard for the Functional Verification Language e, Standard 1647-2011. ANSI/IEEE, New York, 2011.
• [32] Chaochen Z, Hoare CAR, Ravn AP. A Calculus of Durations. Inf. Process. Lett., 1991. 40(5):269-276. doi:10.1016/0020-0190(91)90122-X.
• [33] Linker S, Hilscher M. Proof Theory of a Multi-Lane Spatial Logic. Logical Methods in Computer Science, 2015. 11(3). doi:10.2168/LMCS-11(3:4)2015.
• [34] Klaudel H, Koutny M, Moszkowski BC. From Petri Nets with Shared Variables to ITL. In: Desel J, Yakovlev A (eds.), 16th International Conference on Application of Concurrency to System Design, ACSD 2016, Torun, Poland, June 19-24, 2016. IEEE Computer Society. ISBN 978-1-5090-2589-3, 2016 pp. 11-18. doi:10.1109/ACSD.2016.12.
• [35] Klaudel H, Koutny M, Duan Z. Interval Temporal Logic Semantics of Box Algebra. In: Dediu A, Martín-Vide C, Sierra-Rodríguez JL, Truthe B (eds.), Language and Automata Theory and Applications - 8th International Conference, LATA 2014, Madrid, Spain, March 10-14, 2014. Proceedings, volume 8370 of Lecture Notes in Computer Science. Springer. ISBN 978-3-319-04920-5, 2014 pp. 441-452. doi:10.1007/978-3-319-04921-2_36.
• [36] Esparza J, Nielsen M. Decidability Issues for Petri Nets - a survey. Elektronische Informationsverarbeitung und Kybernetik, 1994. 30(3):143-160.
• [37] Girard J. Linear Logic. Theor. Comput. Sci., 1987. 50:1-102. doi:10.1016/0304-3975(87)90045-4.
• [38] Parigot M, Pelz E. A Logical Approach of Petri Net Languages. Theor. Comput. Sci., 1985. 39:155-169. doi:10.1016/0304-3975(85)90136-7.
• [39] Cau A, Janicke H, Moszkowski BC. Verification and enforcement of access control policies. Formal Methods in System Design, 2013. 43(3):450-492. doi:10.1007/s10703-013-0187-3.
• [40] Cau A, Zedan H. Refining Interval Temporal Logic Specifications. In: Bertran M, Rus T (eds.), Transformation-Based Reactive Systems Development, 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software, ARTS’97, Palma, Mallorca, Spain, May 21-23, 1997, Proceedings, volume 1231 of Lecture Notes in Computer Science. Springer. ISBN 3-540-63010-4, 1997 pp. 79-94. doi:10.1007/3-540-63010-4_6.
• [41] Janicke H, Cau A, Siewe F, Zedan H. Dynamic Access Control Policies: Specification and Verification. Comput. J., 2013. 56(4):440-463. doi:10.1093/comjnl/bxs102.
• [42] Esparza J, Römer S, Vogler W. An Improvement of McMillan’s Unfolding Algorithm. In: Margaria T, Steffen B (eds.), Tools and Algorithms for Construction and Analysis of Systems, Second International Workshop, TACAS ’96, Passau, Germany, March 27-29, 1996, Proceedings, volume 1055 of Lecture Notes in Computer Science. Springer. ISBN 3-540-61042-1, 1996 pp. 87-106. doi:10.1007/3-540-61042-1_40.
• [43] Khomenko V, Koutny M. Towards an Efficient Algorithm for Unfolding Petri Nets. In: Larsen KG, Nielsen M (eds.), CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science. Springer. ISBN 3-540-42497-0, 2001 pp. 366-380. doi:10.1007/3-540-44685-0_25.
• [44] http://www.informatik.uni-hamburg.de/TGI/PetriNets/tools/.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).