×

Quantitative Kleene coalgebras. (English) Zbl 1227.68075

Coalgebras serve as a generic framework for state-based systems, generalizating system types such as deterministic finite automata or labelled transition systems. Finite coalgebras are of particular interest as they relate to generalized notions of a regular language. In earlier work, some of the authors of the current article have provided a language of generalized regular expressions for finite coalgebras of so-called Kripke polynomial functors, generated from the powerset functor, constant functors, and the identity functor by closing under finite sums and products (with some modifications required to propagate semi-lattice structure) [A. Silva, M. Bonsangue and J. Rutten, “Non-deterministic Kleene coalgebras”, Log. Methods Comput. Sci. 6, No. 3, Paper No. 23, 39 p. (2010; Zbl 1208.68141)].
The main results are a generalization of Kleene’s theorem, stating that generalized regular expressions describe exactly the finite coalgebras, as well as a sound and complete equational axiomatization. In the current work, these results are extended to so-called quantitative functors, which additionally allow the use of monoidal exponentiation, i.e., the formation of functors \(M^H\) where \(M\) is a commutative monoid and \(H\) is a quantitative functor. This generalization covers, e.g., various forms of weighted automata. Moreover, expression languages are often easy to restrict to subfunctors; in particular, the method can easily be made to apply to probabilistic systems. Instantiating the generic framework often yields subsets (typically distinguished by the omission of parallel operators) of existing expression languages from the literature.
In some cases, the axiomatization thus obtained is new; this holds in particular for the expression language for weighted automata [P. Buchholz and P. Kemper, “Quantifying the dynamic behavior of process algebras”, Lect. Notes Comput. Sci. 2165, 184–199 (2001; Zbl 1007.68130)] and the expression language for stratified probabilistic systems [R. J. van Glabbeek, S. A. Smolka and B. Steffen, “Reactive, generative and stratified models of probabilistic processes”, Inf. Comput. 121, No. 1, 59–80 (1995; Zbl 0832.68042)].

MSC:

68Q70 Algebraic theory of languages and automata
68Q45 Formal languages and automata
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Software:

CIRC
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Aceto, Luca; Ésik, Zoltán; Ingólfsdóttir, Anna, Equational axioms for probabilistic bisimilarity, (Kirchner, Hélène; Ringeissen, Christophe, AMAST. AMAST, Lecture Notes in Computer Science, vol. 2422 (2002), Springer), 239-253 · Zbl 1275.68099
[2] Jos C.M. Baeten, Jan A. Bergstra, Scott A. Smolka, Axiomization probabilistic processes: Acp with generative probabililties (extended abstract), in: Cleaveland [14], pp. 472-485.; Jos C.M. Baeten, Jan A. Bergstra, Scott A. Smolka, Axiomization probabilistic processes: Acp with generative probabililties (extended abstract), in: Cleaveland [14], pp. 472-485.
[3] Jos C.M. Baeten, Jan Willem Klop (Eds.), in: CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, Lecture Notes in Computer Science, vol. 458, Springer, 1990.; Jos C.M. Baeten, Jan Willem Klop (Eds.), in: CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, Lecture Notes in Computer Science, vol. 458, Springer, 1990. · Zbl 0746.68005
[4] Bandini, Emanuele; Segala, Roberto, Axiomatizations for probabilistic bisimulation, (Orejas, Fernando; Spirakis, Paul G.; van Leeuwen, Jan, ICALP. ICALP, Lecture Notes in Computer Science, vol. 2076 (2001), Springer), 370-381 · Zbl 0986.68073
[5] Bartels, Falk; Sokolova, Ana; de Vink, Erik P., A hierarchy of probabilistic system types, Theor. Comput. Sci., 327, 1-2, 3-22 (2004) · Zbl 1071.68071
[6] Filippo Bonchi, Marcello M. Bonsangue, Jan J.M.M. Rutten, Alexandra Silva, Deriving syntax and axioms for quantitative regular behaviours, in: Bravetti, Zavattaro [10], pp. 146-162.; Filippo Bonchi, Marcello M. Bonsangue, Jan J.M.M. Rutten, Alexandra Silva, Deriving syntax and axioms for quantitative regular behaviours, in: Bravetti, Zavattaro [10], pp. 146-162. · Zbl 1254.68129
[7] Bonsangue, Marcello M.; Rutten, Jan J. M.M.; Silva, Alexandra, Coalgebraic logic and synthesis of Mealy machines, (Amadio, Roberto M., FoSSaCS. FoSSaCS, Lecture Notes in Computer Science, vol. 4962 (2008), Springer), 231-245 · Zbl 1137.68034
[8] Bonsangue, Marcello M.; Rutten, Jan J. M.M.; Silva, Alexandra, An algebra for Kripke polynomial coalgebras, (LICS (2009), IEEE Computer Society), 49-58
[9] Michele Boreale, Weighted bisimulation in linear algebraic form, in: Bravetti, Zavattaro [10], pp. 163-177.; Michele Boreale, Weighted bisimulation in linear algebraic form, in: Bravetti, Zavattaro [10], pp. 163-177. · Zbl 1254.68130
[10] Mario Bravetti, Gianluigi Zavattaro (Eds.), in: CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5710, Springer, 2009.; Mario Bravetti, Gianluigi Zavattaro (Eds.), in: CONCUR 2009 - Concurrency Theory, 20th International Conference, CONCUR 2009, Bologna, Italy, September 1-4, 2009, Proceedings, Lecture Notes in Computer Science, vol. 5710, Springer, 2009.
[11] Brzozowski, Janusz A., Derivatives of regular expressions, J. ACM, 11, 4, 481-494 (1964) · Zbl 0225.94044
[12] Buchholz, Peter, Bisimulation relations for weighted automata, Theor. Comput. Sci., 393, 1-3, 109-123 (2008) · Zbl 1136.68032
[13] Buchholz, Peter; Kemper, Peter, Quantifying the dynamic behavior of process algebras, (de Alfaro, Luca; Gilmore, Stephen, PAPM-PROBMIV. PAPM-PROBMIV, Lecture Notes in Computer Science, vol. 2165 (2001), Springer), 184-199 · Zbl 1007.68130
[14] Rance Cleaveland (Ed.), in: CONCUR ’92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, Lecture Notes in Computer Science, vol. 630, Springer, 1992.; Rance Cleaveland (Ed.), in: CONCUR ’92, Third International Conference on Concurrency Theory, Stony Brook, NY, USA, August 24-27, 1992, Proceedings, Lecture Notes in Computer Science, vol. 630, Springer, 1992.
[15] D’Argenio, Pedro R.; Hermanns, Holger; Katoen, Joost-Pieter, On generative parallel composition, Electr. Notes Theor. Comput. Sci., 22, 30-54 (1999) · Zbl 0920.68078
[16] Deng, Yuxin; Palamidessi, Catuscia, Axiomatizations for probabilistic finite-state behaviors, (Sassone, Vladimiro, FoSSaCS. FoSSaCS, Lecture Notes in Computer Science, vol. 3441 (2005), Springer), 110-124 · Zbl 1119.68125
[17] Deng, Yuxin; Palamidessi, Catuscia; Pang, Jun, Compositional reasoning for probabilistic finite-state behaviors, (Middeldorp, Aart; van Oostrom, Vincent; van Raamsdonk, Femke; de Vrijer, Roel C., Processes, Terms and Cycles. Processes, Terms and Cycles, Lecture Notes in Computer Science, vol. 3838 (2005), Springer), 309-337 · Zbl 1171.68570
[18] Droste, Manfred; Gastin, Paul, Weighted automata and weighted logics, (Caires, Luís; Italiano, Giuseppe F.; Monteiro, Luís; Palamidessi, Catuscia; Yung, Moti, ICALP. ICALP, Lecture Notes in Computer Science, vol. 3580 (2005), Springer), 513-525 · Zbl 1084.03036
[19] Alessandro Giacalone, Chi-Chang Jou, Scott A. Smolka, Algebraic reasoning for probabilistic concurrent systems, in: M. Broy, C.B. Jones (Eds.), Proceedings of Working Conference on Programming Concepts and Methods, IFIP TC 2, 1990.; Alessandro Giacalone, Chi-Chang Jou, Scott A. Smolka, Algebraic reasoning for probabilistic concurrent systems, in: M. Broy, C.B. Jones (Eds.), Proceedings of Working Conference on Programming Concepts and Methods, IFIP TC 2, 1990.
[20] Peter Gumm, H.; Schröder, Tobias, Monoid-labeled transition systems, Electr. Notes Theor. Comput. Sci., 44, 1, 185-204 (2001) · Zbl 1260.68240
[21] Peter Gumm, H.; Schröder, Tobias, Products of coalgebras, Algebra Universalis, 46, 163-185 (2001) · Zbl 1061.18005
[22] Peter Gumm, H.; Schröder, Tobias, Coalgebras of bounded type, Math. Struct. Comput. Sci., 12, 5, 565-578 (2002) · Zbl 1011.08009
[23] Hansson, Hans; Jonsson, Bengt, A logic for reasoning about time and reliability, Formal Asp. Comput., 6, 5, 512-535 (1994) · Zbl 0820.68113
[24] Chi-Chang Jou, Scott A. Smolka, Equivalences, congruences, and complete axiomatizations for probabilistic processes, in: Baeten, Klop [3], pp. 367-383.; Chi-Chang Jou, Scott A. Smolka, Equivalences, congruences, and complete axiomatizations for probabilistic processes, in: Baeten, Klop [3], pp. 367-383.
[25] Kleene, Stephen, Representation of events in nerve nets and finite automata, Autom. Stud., 3-42 (1956)
[26] Klin, Bartek, Structural operational semantics for weighted transition systems, (Palsberg, Jens, Semantics and Algebraic Specification. Semantics and Algebraic Specification, Lecture Notes in Computer Science, vol. 5700 (2009), Springer), 121-139 · Zbl 1253.68214
[27] Dexter Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, in: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, LICS, IEEE Computer Society, Amsterdam, The Netherlands, 1991, pp. 214-225.; Dexter Kozen, A completeness theorem for Kleene algebras and the algebra of regular events, in: Proceedings, Sixth Annual IEEE Symposium on Logic in Computer Science, 15-18 July, LICS, IEEE Computer Society, Amsterdam, The Netherlands, 1991, pp. 214-225.
[28] Larsen, Kim Guldstrand; Skou, Arne, Bisimulation through probabilistic testing, Inform. Comput, 94, 1, 1-28 (1991) · Zbl 0756.68035
[29] Kim Guldstrand Larsen, Arne Skou, Compositional verification of probabilistic processes, in: Cleaveland [14], pp. 456-471.; Kim Guldstrand Larsen, Arne Skou, Compositional verification of probabilistic processes, in: Cleaveland [14], pp. 456-471.
[30] Lucanu, Dorel; Goriac, Eugen-Ioan; Caltais, Georgiana; Rosu, Grigore, Circ: a behavioral verification tool based on circular coinduction, (Kurz, Alexander; Lenisa, Marina; Tarlecki, Andrzej, CALCO. CALCO, Lecture Notes in Computer Science, vol. 5728 (2009), Springer), 433-442 · Zbl 1239.68066
[31] Milner, Robin, A complete inference system for a class of regular behaviours, J. Comput. Syst. Sci., 28, 3, 439-466 (1984) · Zbl 0562.68065
[32] Mislove, Michael W.; Ouaknine, Joël; Worrell, James, Axioms for probability and nondeterminism, Electr. Notes Theor. Comput. Sci., 96, 7-28 (2004) · Zbl 1271.68192
[33] Pnueli, Amir; Zuck, Lenore D., Probabilistic verification by tableaux, (LICS (1986), IEEE Computer Society), 322-331 · Zbl 0797.68112
[34] Rabin, Michael O., Probabilistic automata, Inform. Control, 6, 3, 230-245 (1963) · Zbl 0182.33602
[35] Rutten, Jan J. M.M., Universal coalgebra: a theory of systems, Theor. Comput. Sci., 249, 1, 3-80 (2000) · Zbl 0951.68038
[36] Rutten, Jan J. M.M., Coalgebraic foundations of linear systems, (Mossakowski, Till; Montanari, Ugo; Haveraaen, Magne, CALCO. CALCO, Lecture Notes in Computer Science, vol. 4624 (2007), Springer), 425-446 · Zbl 1214.68232
[37] Salomaa, Arto, Two complete axiom systems for the algebra of regular events, J. ACM, 13, 1, 158-169 (1966) · Zbl 0149.24902
[38] Schützenberger, Marcel Paul, On the definition of a family of automata, Inform. Control, 4, 2-3, 245-270 (1961) · Zbl 0104.00702
[39] Roberto Segala, Modeling and Verification of Randomized Distributed Real-time Systems, Ph.D. thesis, MIT, Department of EECS, 1995.; Roberto Segala, Modeling and Verification of Randomized Distributed Real-time Systems, Ph.D. thesis, MIT, Department of EECS, 1995. · Zbl 1374.68296
[40] Segala, Roberto; Lynch, Nancy A., Probabilistic simulations for probabilistic processes, (Jonsson, Bengt; Parrow, Joachim, CONCUR. CONCUR, Lecture Notes in Computer Science, vol. 836 (1994), Springer), 481-496 · Zbl 0839.68067
[41] Scott A. Smolka, Bernhard Steffen, Priority as extremal probability, in: Baeten, Klop [3], pp. 456-466.; Scott A. Smolka, Bernhard Steffen, Priority as extremal probability, in: Baeten, Klop [3], pp. 456-466. · Zbl 0860.68027
[42] Stark, Eugene W.; Smolka, Scott A., A complete axiom system for finite-state probabilistic processes, (Plotkin, Gordon D.; Stirling, Colin; Tofte, Mads, Proof, Language, and Interaction (2000), The MIT Press), 571-596
[43] Turi, Daniele; Rutten, Jan J. M.M., On the foundations of final coalgebra semantics: non-well-founded sets, partial orders, metric spaces, Math. Struct. Comput. Sci., 8, 5, 481-540 (1998) · Zbl 0917.68140
[44] van Breugel, Franck; Worrell, James, Approximating and computing behavioural distances in probabilistic transition systems, Theor. Comput. Sci., 360, 1-3, 373-385 (2006) · Zbl 1097.68102
[45] van Glabbeek, Rob J.; Smolka, Scott A.; Steffen, Bernhard, Reactive, generative and stratified models of probabilistic processes, Inform. Comput., 121, 1, 59-80 (1995) · Zbl 0832.68042
[46] Vardi, Moshe Y., Automatic verification of probabilistic concurrent finite-state programs, (FOCS (1985), Springer), 327-338
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.