×

zbMATH — the first resource for mathematics

Complete proof systems for weighted modal logic. (English) Zbl 1317.68120
Weighted Modal Logic (WML) is a multi-modal logic that expresses qualitative and quantitative properties of Weighted Transition Systems (WTS), i.e., the transition systems having both states and transitions labeled with real numbers: the state labels denote quantitative resources, while the transition labels denote costs of transitions in terms of resources. Here, both weak-complete and strong-complete axiomatizations for WML against WTSs is proposed as well as a series of metatheorems including the finite model property and the existence of canonical models. It is shown how the proof system can be used in the context of a process algebra semantics for WML to convert a model-checking problem in to a theorem-proving problem.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B45 Modal logic (including the logic of norms)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Rajeev Alur, David L. Dill, Automata for modeling real-time systems, in: Paterson [25], pp. 322-335. · Zbl 0765.68150
[2] Rajeev Alur, Salvatore La Torre, George J. Pappas, Optimal paths in weighted timed automata, in: Benedetto and Sangiovanni-Vincentelli [7], pp. 49-62. · Zbl 0991.93076
[3] Reif Andersen, Henrik; Stirling, Colin; Winskel, Glynn, A compositional proof system for the modal mu-calculus, (LICS, (1994), IEEE Computer Society), 144-153
[4] Henrik Reif Andersen, Glynn Winskel, Compositional checking of satisfaction, in: Larsen and Skou [21], pp. 24-36. · Zbl 0776.68083
[5] (Ausiello, Giorgio; Dezani-Ciancaglini, Mariangiola; Ronchi Della Rocca, Simona, Proceedings of the Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Lecture Notes in Computer Science, vol. 372, (1989), Springer) · Zbl 0681.00016
[6] Gerd Behrmann, Ansgar Fehnker, Thomas Hune, Kim Guldstrand Larsen, Paul Pettersson, Judi Romijn, Frits W. Vaandrager, Minimum-cost reachability for priced timed automata, in: Benedetto and Sangiovanni-Vincentelli [7], pp. 147-161. · Zbl 0991.68037
[7] (Di Benedetto, Maria Domenica; Sangiovanni-Vincentelli, Alberto L., Proceedings of the Hybrid Systems: Computation and Control, 4th International Workshop, HSCC 2001, Rome, Italy, March 28-30, 2001, Lecture Notes in Computer Science, vol. 2034, (2001), Springer) · Zbl 0990.00076
[8] Cardelli, Luca; Larsen, Kim G.; Mardare, Radu, Continuous Markovian logic - from complete axiomatization to the metric space of formulas, (Bezem, Marc, CSL, LIPIcs, vol. 12, (2011), Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik), 144-158 · Zbl 1247.03030
[9] Cleaveland, Rance; Steffen, Bernhard, Computing behavioural relations, logically, (Leach Albert, Javier; Monien, Burkhard; Rodríguez-Artalejo, Mario, ICALP, Lecture Notes in Computer Science, vol. 510, (1991), Springer), 127-138 · Zbl 0769.68024
[10] Rance Cleaveland, Bernhard Steffen, A linear-time model-checking algorithm for the alternation-free modal mu-calculus, in: Larsen and Skou [21], pp. 48-58. · Zbl 0772.68038
[11] (Droste, Manfred; Kuich, Werner; Vogler, Heiko, Handbook of Weighted Automata, (2009), Springer-Verlag)
[12] Goldblatt, Robert, Deduction systems for coalgebras over measurable spaces, J. Logic Comput., 20, 5, 1069-1100, (2010) · Zbl 1220.03054
[13] Goldblatt, Robert, Topological proofs of some rasiowa-sikorski lemmas, Studia Logica, 100, 1-2, 175-191, (2012) · Zbl 1259.06009
[14] Hennessy, Matthew; Milner, Robin, Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 1, 137-161, (1985) · Zbl 0629.68021
[15] Hoare, C. A.R., Communicating sequential processes, (1985), Prentice-Hall · Zbl 0637.68007
[16] Kozen, Dexter, Results on the propositional μ-calculus, (Nielsen, Mogens; Meineche Schmidt, Erik, ICALP, Lecture Notes in Computer Science, vol. 140, (1982), Springer), 348-359 · Zbl 0507.03005
[17] Kozen, Dexter; Larsen, Kim G.; Mardare, Radu; Panangaden, Prakash, Stone duality for Markov processes, (LICS, (2013), IEEE Computer Society), 321-330 · Zbl 1433.06006
[18] Larsen, Kim G., Context-dependent bisimulation between processes, (1986), Edinburgh University, PhD thesis
[19] Larsen, Kim Guldstrand, Proof system for hennessy-milner logic with recursion, (Dauchet, Max; Nivat, Maurice, CAAP, Lecture Notes in Computer Science, vol. 299, (1988), Springer), 215-230
[20] Larsen, Kim Guldstrand, Ideal specification formalism + expressivity + compositionality + decidability + testability + …, (Baeten, Jos C. M.; Klop, Jan Willem, CONCUR, Lecture Notes in Computer Science, vol. 458, (1990), Springer), 33-56
[21] (Larsen, Kim Guldstrand; Skou, Arne, Proceedings of the Computer Aided Verification, 3rd International Workshop, CAV ’91, Aalborg, Denmark, July 1-4, 1991, Lecture Notes in Computer Science, vol. 575, (1992))
[22] Kim Guldstrand Larsen, Liu Xinxin, Compositionality through an operational semantics of contexts, in: Paterson [25], pp. 526-539. · Zbl 0765.68107
[23] Mardare, Radu; Cardelli, Luca; Larsen, Kim G., Continuous Markovian logics - axiomatization and quantified metatheory, Log. Methods Comput. Sci., 8, 4, (2012) · Zbl 1261.03088
[24] Milner, Robin, A calculus of communicating systems, Lecture Notes in Computer Science, vol. 92, (1980), Springer · Zbl 0452.68027
[25] (Paterson, Mike, Proceedings of the Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, July 16-20, 1990, Lecture Notes in Computer Science, vol. 443, (1990), Springer)
[26] Bernhard Steffen, Characteristic formulae, in: Ausiello et al. [5], pp. 723-732.
[27] Steffen, Bernhard; Ingólfsdóttir, Anna, Characteristic formulae for processes with divergence, Inform. and Comput., 110, 1, 149-163, (1994) · Zbl 0804.68097
[28] Stirling, Colin; Walker, David, Local model checking in the modal mu-calculus, (Díaz, Josep; Orejas, Fernando, TAPSOFT, Lecture Notes in Computer Science, vol. 1, (1989), Springer), 369-383
[29] Walukiewicz, Igor, Completeness of Kozen’s axiomatisation of the propositional mu-calculus, (LICS, (1995), IEEE Computer Society), 14-24 · Zbl 1046.68628
[30] Winskel, Glynn, On the composition and decomposition of assertions, (Brookes, Stephen D.; Roscoe, A. W.; Winskel, Glynn, Seminar on Concurrency, Lecture Notes in Computer Science, vol. 197, (1984), Springer), 62-75 · Zbl 0567.68014
[31] Winskel, Glynn, A complete system for SCCS with modal assertions, (Maheshwari, S. N., FSTTCS, Lecture Notes in Computer Science, vol. 206, (1985), Springer), 392-410 · Zbl 0586.68024
[32] Glynn Winskel, A note on model checking the modal nu-calculus, in: Ausiello et al. [5], pp. 761-772.
[33] Zhou, Chunlai, A complete deductive system for probability logic, J. Logic Comput., 19, 6, 1427-1454, (2009) · Zbl 1191.03018
[34] Zhou, Chunlai, Intuitive probability logic, (Ogihara, Mitsunori; Tarui, Jun, TAMC, Lecture Notes in Computer Science, vol. 6648, (2011), Springer), 240-251 · Zbl 1258.03025
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.