Abstract
We extend recent work on defining linear-time behaviour for state-based systems with branching, and propose modal and fixpoint logics for specifying linear-time temporal properties of states in such systems. We model systems with branching as coalgebras whose type arises as the composition of a branching monad and a polynomial endofunctor on the category of sets, and employ a set of truth values induced canonically by the branching monad. This yields logics for reasoning about quantitative aspects of linear-time behaviour. Examples include reasoning about the probability of a linear-time behaviour being exhibited by a system with probabilistic branching, or about the minimal cost of a linear-time behaviour being exhibited by a system with weighted branching. In the case of non-deterministic branching, our logic supports reasoning about the possibility of exhibiting a given linear-time behaviour, and therefore resembles an existential version of the logic LTL.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)
Cîrstea, C.: From Branching to Linear Time, Coalgebraically. In: Baelde, D., Carayol, A. (eds.) Proc. FICS 2013. EPTCS, vol. 126, pp. 11–27 (2013)
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)
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order, 2nd edn. Cambridge University Press (2002)
Hermida, C., Jacobs, B.: Structural induction and coinduction in a fibrational setting. Inf. Comput. 145(2), 107–152 (1998)
Jacobs, B.: Introduction to coalgebra. Towards mathematics of states and observations (version 2.0). Draft (2012)
Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990)
Kock, A.: Monads and extensive quantities, arXiv:1103.6009 (2011)
Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309(1-3), 177–193 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cîrstea, C. (2014). A Coalgebraic Approach to Linear-Time Logics. In: Muscholl, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2014. Lecture Notes in Computer Science, vol 8412. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-54830-7_28
Download citation
DOI: https://doi.org/10.1007/978-3-642-54830-7_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-54829-1
Online ISBN: 978-3-642-54830-7
eBook Packages: Computer ScienceComputer Science (R0)