Łukasiewicz μ-calculus

• Autorzy: Mio M. , Simpson A.

Identyfikatory

DOI

10.3233/FI-2017-1472

• Języki publikacji: EN

Abstrakty

EN

The paper explores properties of the Łukasiewicz μ-calculus, or Łμ for short, an extension of Łukasiewicz logic with scalar multiplication and least and greatest fixed-point operators (for monotone formulas). We observe that Łμ terms, with n variables, define monotone piece-wise linear functions from [0, 1]n to [0, 1]. Two effective procedures for calculating the output of Łμ terms on rational inputs are presented. We then consider the Łukasiewicz modal μ-calculus, which is obtained by adding box and diamond modalities to Łμ. Alternatively, it can be viewed as a generalization of Kozen’s modal μ-calculus adapted to probabilistic nondeterministic transition systems (PNTS’s). We show how properties expressible in the well-known logic PCTL can be encoded as Łukasiewicz modal μ-calculus formulas. We also show that the algorithms for computing values of Łukasiewicz μ-calculus terms provide automatic (albeit impractical) methods for verifying Łukasiewicz modal μ-calculus properties of finite rational PNTS’s.

Słowa kluczowe

EN

Łukasiewicz logic; probabilistic μ-calculus; model checking; PCTL; probabilistic temporal logic

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 3/4
• Strony: 317--346
• Opis fizyczny: Bibliogr. 36 poz., wykr.

Twórcy

autor

Mio M.

• Laboratoire de l’Informatique du Parallèlisme, CNRS and École Normale Supérieure de Lyon, France

autor

Simpson A.

• Faculty of Mathematics and Physics, University of Ljubljana, Slovenia

Bibliografia

• [1] Nola AD, Leustean I. Riesz MV-algebras and their logic. In: Proceeding of Conference of the European Society for Fuzzy Logic and Technology (EUSFLAT), pp. 140-145. Atlantis Press, 2011. doi: 10.2991/eusflat.2011.125.
• [2] Spada L. μMV-algebras: An approach to fixed points in Łukasiewicz logic. Fuzzy Sets and Systems, 2008; 159 (10): 1260-1267. doi: 10.1016/j.fss.2007.12.010.
• [3] Kozen D. Results on the Propositional mu-Calculus. Theoretical Computer Science, 1983; 27 (3): 333-354. doi: 10.1016/0304-3975(82)90125-6.
• [4] Janin D, Walukiewicz I. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. Lecture Notes in Computer Science, 1996; 1119: 263-277. doi: 10.1007/3-540-61604-7\_60.
• [5] Segala R. Modeling and Verification of Randomized Distributed Real-Time Systems. Ph.D. thesis. MIT, 1995.
• [6] Huth M, Kwiatkowska M. Quantitative Analysis and Model Checking. In: Proceedings of IEEE Symposium on Logic in Computer Science (LICS), pp. 111-122. IEEE, 1997. doi: 10.1109/LICS.1997.614940.
• [7] Morgan C, McIver A. A Probabilistic Temporal Calculus Based on Expectations. In: Proceedings of Formal Methods Pacific, pp. 4-22. Springer-Verlag, 1997.
• [8] McIver A, Morgan C. Results on the quantitative μ-calculus qMμ. ACM Transactions on Computational Logic, 2007; 8 (1). doi: 10.1145/1182613.1182616.
• [9] Mio M. On The Equivalence of Denotational and Game Semantics for the Probabilistic μ-Calculus. Logical Methods in Computer Science, 2012; 8 (2): 1-21. doi: 10.2168/LMCS-8(2:7)2012.
• [10] Bianco A, de Alfaro L. Model Checking of Probabilistic and Nondeterministic Systems. In: Proceedings of Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 1026 of Lecture Notes in Computer Science, pp. 499-513. Springer Berlin Heidelberg, 1995. doi: 10.1007/3-540- 60692-0\_70.
• [11] Mio M. Probabilistic Modal μ-Calculus with Independent Product. Logical Methods in Computer Science, 2012; 8 (4): 1-36. doi: 10.2168/LMCS-8(4:18)2012.
• [12] Mio M. Game Semantics for Probabilistic μ-Calculi. Ph.D. thesis, School of Informatics, University of Edinburgh, 2012.
• [13] Baier C. Katoen JP. Principles of Model Checking. The MIT Press, 2008.
• [14] Hájek P. Metamathematics of Fuzzy Logic. Springer, 2001. ISBN 1402003706. doi: 10.1007/978-94-011-5300-3.
• [15] Mundici D. Advanced Łukasiewicz Calculus and MV-Algebras. Trends in Logic. Springer-Verlag, 2011. doi: 10.1007/978-94-007-0840-2.
• [16] Gerla. B. Rational Łukasiewicz logic and DMV-algebras. Neural Networks World, 2001; pp. 579-584.
• [17] Gerla. B. Rational Łukasiewicz logic and DMV-algebras, 2012. ArXiv: 1211.5485.
• [18] Stirling C. Modal and temporal logics for processes. Springer, 2001. ISBN 978-0-387-98717-0.
• [19] Ferrante J, Rackoff C. A Decision Procedure for the First Order Theory of Real Addition with Order. SIAM Journal of Computing, 1975; 4 (1): 69—76. doi: 10.1137/0204006.
• [20] Boigelot B, Jodogne S, Wolper P. An effective decision procedure for linear arithmetic over the integers and reals. ACM Transactions on Computational Logic, 2005; 6 (13): 614-633. doi: 10.1145/1071596.1071601.
• [21] McNaughton R. A theorem about infinite-valued sentential logic. The Journal of Symbolic Logic, 1951; 16: 1-13. doi: 10.2307/2268660.
• [22] Cintula P, Kroupa T. Simple games in Łukasiewicz calculus and their cores. Kybernetika, 2013; 3: 404-419. URL http://eudml.org/doc/260726.
• [23] Blum L, Shub M, Smale S. On a Theory of Computation and Complexity over the Real Numbers: NP-completeness, Recursive Functions and Universal Machines. Bulletin of the AMS, 1989; 21 (1): 1-46. doi: 10.1109/SFCS.1988.21955.
• [24] de Alfaro L, Majumdar R. Quantitative solution of omega-regular games. Journal of Computer and System Sciences, 2004; 68: 374-397. doi: 10.1016/j.jcss.2003.07.009.
• [25] Mader A. Modal μ-Calculus, Model Checking and Gauß Elimination. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1217 of Lecture Notes in Computer Science, pp. 72-88. Elsevier, 1995. doi: 10.1007/3-540-60630-0\_4.
• [26] Cleaveland R, Iyer SP, Narasimha M. Probabilistic Temporal Logics via the Modal Mu-Calculus. In: Proceedings of the Second International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), pp. 288-305. Springer-Verlag London, 1999. doi: 10.1007/3-540-49019-1\_20.
• [27] Galwitza TM, Seidl H. Solving Systems of Rational Equations through Strategy Iteration. ACM Transactions on Programming Languages and Systems, 2011; 33 (3): 11-48. doi: 10.1145/1961204.1961207.
• [28] Condon A. The Complexity of Stochastic Games. Information and Computation, 1992; 96: 203-224. doi: 10.1016/0890-5401(92)90048-k.
• [29] Spada L. ŁII logic with fixed points. Archive for Mathematical Logic, 2008; 47: 1260-1267. doi: 10.1007/s00153-008-0105-3.
• [30] Mio M. Upper-Expectation Bisimilarity and Łukasiewicz μ-Calculus. In: Proceedings of Foundations of Software Science and Computation Structures (FoSSaCS), volume 8412 of Lecture Notes in Computer Science, pp. 335-350. Elsevier, 2014. doi: 10.1007/978-3-642-54830-7\_22.
• [31] Deng Y, van Glabbeek R. Characterising Probabilistic Processes Logically. In: Proceedings of Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 6397 of Lecture Notes in Computer Science, pp. 278-293. Springer, 2010. doi: 10.1007/978-3-642-16242-8\_20.
• [32] Walukiewicz I. Completeness of Kozen’s Axiomatisation of the Propositional μ-Calculus. Information and Computation, 2000. 157. doi: 10.1006/inco.1999.2836.
• [33] Delahaye B, Katoen JP, Larsen K, Legay A, Pedersen M, Sher F, Wasowski A. Abstract Probabilistic Automata. Information and Computation, 2013; 232: 66-116. doi: 10.1016/j.ic.2013.10.002.
• [34] Kwiatkowska M, Norman G, Parker D, Qu H. Assume-Guarantee Verification for Probabilistic Systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6015 of Lecture Notes in Computer Science, pp. 23-37. Springer, 2010. doi: 10.1007/978-3-642-12001-2_3.
• [35] Forejt V, Kwiatkowska M, Norman G, Parker D, Qu H. Quantitative multi-objective verification for probabilistic systems. In: Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 6605 of Lecture Notes in Computer Science, pp. 112-127. Springer, 2011. doi: 10.1007/978-3-642-19835-9\_11.
• [36] Huth M, Piterman N, Wagner D. p-Automata: New Foundations for discrete-time Probabilistic Verification. Performance Evaluation, 2012; 69 (7-8): 356-378. doi: 10.1016/j.peva.2012.05.005.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę (zadania 2017).