Abstract
We extend the theory of maximal traces of pointed non-deterministic coalgebras by providing an automata-based characterisation of the set of maximal traces for finite such coalgebras. We then consider linear coalgebraic temporal logics interpreted over non-deterministic coalgebras, and show how to reduce the model checking problem for such logics to the problem of deciding the winner in a regular two-player game. Our approach is inspired by the automata-theoretic approach to model checking Linear Temporal Logic over transition systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Baltag, A.: A logic for coalgebraic simulation. In: Proc. CMCS 2000. Electr. Notes Theor. Comput. Sci., vol. 33, pp. 42–60 (2000)
Cîrstea, C.: Generic infinite traces and path-based coalgebraic temporal logics. In: Proc. CMCS 2010. Electr. Notes Theor. Comput. Sci., vol. 264, pp. 83–103 (2010)
Fontaine, G., Leal, R., Venema, Y.: Automata for coalgebras: an approach using predicate liftings. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010. LNCS, vol. 6199, pp. 381–392. Springer, Heidelberg (2010)
Jacobs, B.: Trace semantics for coalgebras. In: Proc. CMCS 2004. Electr. Notes Theor. Comput. Sci., vol. 106, pp. 167–184 (2004)
Kupke, C., Venema, Y.: Coalgebraic automata theory: basic results. Logical Methods in Computer Science 4(4) (2008)
Mazala, R.: 2 infinite games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 23–38. Springer, Heidelberg (2002)
Vardi, M.: Automata-theoretic techniques fo temporal reasoning. In: Handbook of Modal Logic, pp. 971–990. Addison Wesley, Reading (2005)
Venema, Y.: Automata and fixed point logics: a coalgebraic perspective. Information and Computation 204, 637–678 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cîrstea, C. (2011). Model Checking Linear Coalgebraic Temporal Logics: An Automata-Theoretic Approach. In: Corradini, A., Klin, B., Cîrstea, C. (eds) Algebra and Coalgebra in Computer Science. CALCO 2011. Lecture Notes in Computer Science, vol 6859. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22944-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-22944-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22943-5
Online ISBN: 978-3-642-22944-2
eBook Packages: Computer ScienceComputer Science (R0)