Modal and Temporal Logics

Publisher Website
Google Scholar
Abstract
In achieving their goals, programs manipulate data and thereby may change th state of the computer. Regarded as a dynamic system, the computer responds to program instructions and in so doing may change state. Activity and change are formalized by the operational semantics of programs and systems. Modal and temporal logics can directly express activity with their paradigm operators such as [a) (box a) when a is an action, and F. Where Φ is a proposition, [a)Φ expresses after every a action Φ holds while FΦ expresses eventually Φ holds. The modal operator [a] highlights the action that may provoke change of state whereas the temporal operator F focuses on the resulting changes. In both cases these operators may express properties of events that happen during a run of a system, events that may be crucial to understanding its overall behaviour. It is no accident that these logics can be used to express such notions. For their models comprehend structures that are encountered in operational semantics of programs and systems. These structures, (labelled) transition systems, are pivotal to this chapter.

This publication has 0 references indexed in Scilit: