From Branching to Linear Time, Coalgebraically

• Autorzy: Cîrstea C.

Identyfikatory

DOI

10.3233/FI-2017-1474

• Języki publikacji: EN

Abstrakty

EN

We consider state-based systems modelled as coalgebras whose type incorporates branching, and show that suitably adapting the definition of coalgebraic bisimulation yields a general and uniform account of the linear-time behaviour of a state in such a coalgebra. By moving away from a boolean universe of truth values, our approach can measure the extent to which a state in a system with branching is able to exhibit a particular linear-time behaviour. This instantiates to measuring the probability of a specific behaviour occurring in a probabilistic system, or measuring the minimal cost of exhibiting a given behaviour in the case of weighted computations.

Słowa kluczowe

EN

coalgebra; linear time; trace

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 150, nr 3/4
• Strony: 379--406
• Opis fizyczny: Bibliogr. 25 poz., rys.

Twórcy

autor

Cîrstea C.

• Electronics and Computer Science, University of Southampton, United Kingdom

Bibliografia

• [1] Rutten JJMM. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 2000. 249 (1): 3-80. doi: 1016/S0304-3975(00)00056-6.
• [2] Hasuo I, Jacobs B, Sokolova A. Generic Trace Semantics via Coinduction. Log. Methods Comput. Sci., 2007. 3 (4): 1-36. doi: 10.2168/LMCS-3(4:11)2007.
• [3] Jacobs B, Silva A, Sokolova A. Trace Semantics via Determinization. In: Proceedings CMCS 2012, volume 7399 of Lect. Notes Comput. Sci., pp. 109-129. Springer, 2012. doi: 10.1007/978-3-642-32784-l_7.
• [4] Jacobs B. Trace Semantics for Coalgebras. In: Proceedings CMCS 2004, volume 106 of Electr. Notes Theor. Comput. Sci., pp. 167-184. Elsevier, 2004. doi: 10.1016/j.entcs.2004.02.031.
• [5] Kerstan H, König B. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems. Logical Methods in Computer Science, 2013. 9 (4). doi: 10.2168/lmcs-9(4:16)2013.
• [6] Cîrstea, C. Maximal Traces and Path-Based Coalgebraic Temporal Logics. Theor. Comput. Sci., 2011. 412 (38): 5025-5042. doi: 10.1016/j.tcs.2011.04.025.
• [7] Hermida C, Jacobs B. Structural Induction and Coinduction in a Fibrational Setting. Inf. Comput., 1998. 145 (2): 107-152. doi: 10.1006/inco.1998.2725.
• [8] Coumans D, Jacobs B. Scalars, Monads, and Categories. In: Heunen C, Sadrzadeh M, Grefenstette E (eds.), Quantum Physics and Linguistics. A Compositional, Diagrammatic Discourse, pp. 184-216. Oxford Univ. Press, 2013. doi: 10.1093/acprof:oso/9780199646296.003.0007.
• [9] Kock A. Monads and extensive quantities, 2011. ArXiv: 1103.6009.
• [10] Cîrstea, C. A Coalgebraic Approach to Linear-Time Logics. In: Proceedings FOSSACS 2014, volume 8412 of Lect. Notes Comput. Sci., pp. 428-442. Springer, 2014. doi: 10.1007/978-3-642-54830-7_28.
• [11] Kanellakis PC, Smolka SA. CCS Expressions, Finite State Processes, and Three Problems of Equivalence. Inf. Comput., 1990. 86 (l): 43-68. doi: 10.1016/0890-5401(90)90025-D.
• [12] Cîrstea, C. From Branching to Linear Time, Coalgebraically. In: Baelde D, Carayol A (eds.), Proceedings FICS 2013, volume 126 of Electron. Proc. Theor. Comput. Sci., pp. 11-27. 2013. doi: 10.4204/EPTCS.126.2.
• [13] Cîrstea, C. Model Checking Linear Coalgebraic Temporal Logics: An Automata-Theoretic Approach. In: Corradini A, Klin B, Cîrstea, C. (eds.), Proceedings CALCO 2011, volume 6859 of Lect. Notes Comput. Sci., pp. 130-144. Springer, 2011. doi: 10.1007/978-3-642-22944-2_10.
• [14] Hasuo I, Cho K, Kataoka T, Jacobs B. Coinductive Predicates and Final Sequences in a Fibration. In: Proceedings MFPS XXIX, volume 298 of Electr. Notes Theor. Comput. Sci., pp. 197-214. Elsevier. 2013. doi: 10.1016/j.entcs.2013.09.014.
• [15] Jacobs B. Introduction to Coalgebra. Towards Mathematics of States and Observations (Version 2.0), 2012. Available from: http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf.
• [16] Pattinson D. Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci., 2003. 309 (1-3): 177-193. doi: 10.1016/S0304-3975(03)00201-9.
• [17] Moss LS. Coalgebraic Logic. Ann. Pure Appl. Logic, 1999. 96 (l-3): 277-317. doi: 10.1016/S0168-0072(98)00042-6.
• [18] Sangiorgi D. On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst., 2009. 31 (4). doi: 10.1145/1516507.1516510.
• [19] Ésik Z, Kuich W. Modern Automata Theory, 2007. Available from: URL http://dmg.tuwien.ac.at/kuich/.
• [20] Fumex C, Ghani N, Johann P. Indexed Induction and Coinduction, Fibrationally. In: Corradini A, Klin B, Cîrstea, C. (eds.), Proceedings CALCO 2011, volume 6859 of Lect. Notes Comput. Sci., pp. 176-191. Springer, 2011. doi: 10.1007/978-3-642-22944-2_13.
• [21] Ghani N, Johann P, Fumex C. Generic Fibrational Induction. Log. Methods Comput. Sci., 2012. 8 (2). doi: 10.2168/LMCS-8(2:12)2012.
• [22] Kock A. Commutative monads as a theory of distributions. Theory and Applications of Categories, 2012. 26 (4): 97—131.
• [23] Davey BA, Priestley HA. Introduction to Lattices and Order (2. ed.). Cambridge University Press, 2002. doi: 10.1017/CB09780511809088.
• [24] Kwiatkowska M, Parker D. Advances in Probabilistic Model Checking. In: Nipkow T, Grumberg O, Hauptmann B (eds.), Software Safety and Security - Tools for Analysis and Verification, volume 33 of NATO Science for Peace and Security Series - D: Information and Communication Security. IOS Press, 2012, pp. 126-151. URL https://hal.inria.fr/hal-00664777.
• [25] Cîrstea, C. Canonical Coalgebraic Linear Time Logics. In: Moss L, Sobocinski P (eds.), Proceedings CALCO 2015, Leibniz International Proceedings in Informatics, pp. 66-85. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015. doi: 10.4230/LIPIcs.CALCO.2015.66.

Uwagi

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