A Unified Perspective of Linear Time Logics using Coalgebras

Add to your list(s) Download to your calendar using vCal

• Corina Cirstea (Southampton)
• Friday 27 April 2018, 11:00-12:00
• Computer Science, The Sloman Lounge (UG).

If you have a question about this talk, please contact Paul Taylor.

We describe a principled approach to deriving linear time logics for a wide variety of state-based, quantitative models, by modelling the latter as coalgebras whose type incorporates both branching and linear behaviour. We define logics whose domain of truth values is determined by the choice of (quantitative) branching, and we provide two equivalent semantics for them: a path-based semantics akin to those of standard linear time logics, and a step-wise semantics that is more amenable to (automata-based) model checking. We also provide a semantic characterisation of the associated notion of logical equivalence. Instances of our logics support reasoning about the possibility, probability or minimal cost of exhibiting a given linear time property. We conclude with a generalisation of our logics, dual in spirit to logics with discounting, which increases their practical appeal in the context of resource-aware computation.

Hosted by Paul Levy

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Computer Science, The Sloman Lounge (UG)
• Theoretical computer science seminar
• computer sience

Note that ex-directory lists are not shown.