Martin Lange: Extended Computation Tree Logic
03.11.2009 10:15
We introduce a generic extension of the standard computation tree logic
CTL in which the Until operator is parametrized by a formal language of
finite words constraining the moments along a path at which this until
may be fulfilled. We briefly motivate the use of such logics and then
focus on decidability and complexity results for the satisfiability and
model checking problems, and on expressive power of these logics.
This is work in progress with Roland Axelsson and Markus Latte, as well
as Matthew Hague and Stephan Kreutzer of Oxford University.
