1 June 2009
Wiebe van der Hoek on Temporal Logic
Posted by Rasmus Rendsvig under: Glossary; Research Axes; Temporal Logic .
Temporal logics provide tools to analyse systems that change over time, tools that can be used by a designer of the changes (computations) in a system or by an analyst, observing the changes (evolution). They are increasingly popular a the language for model checking complex systems, ensuring properties known as liveness (`EVENTUALLY, all is fine’) and safety (`NEVER are we in trouble’) and fairness (IF a request is made, BEFORE LONG it will be granted’). Temporal logics and their semantics also provide ways to systematically study different notions of time, like linear, branching, linear in the past but branching in the future, discrete or continuous, etc.
Like with so many other notions that are studied from a logical perspective, temporal notions become conceptually even more interesting and technically more involved when studied in combination with other notions. For instance, together with agency or actions, one can study notions like synchronous and a-synchronous systems, and combined with knowledge a wide scope of different assumptions (perfect recall, learning, unique starting point, central clock, etc) present a wide range of systems, which, from a logical perspective, show a very varied range of behaviour, from for instance feasible to undecidable.
Wiebe van der Hoek
Loading... 
