State/event based versus purely Action or State based Logics

TL;DR

This paper introduces UCTL* logic, extending state/event based logics, and compares its expressiveness to existing fragments, also applying it to modal transition systems for future research.

Contribution

The paper defines UCTL* logic, proves its expressiveness is equivalent to existing fragments, and adapts it for modal transition systems, advancing the study of state/event based logics.

Findings

UCTL* is not more expressive than existing fragments.

Defined a state/event logic over modified modal transition systems.

Established a foundation for future work in state/event based logics.

Abstract

Although less studied than purely action or state based logics, state/event based logics are becoming increasingly important. Some systems are best studied using structures with information on both states and transitions, and it is these structures over which state/event based logics are defined. The logic UCTL and its variants are perhaps the most widely studied and implemented of these logics to date. As yet, however, no-one seems to have defined UCTL*, a trivial step but a worthwhile one. Here we do just that, but prove in the cases of both UCTL and UCTL* that these logics are no more expressive than their more commonplace fragments. Also, acknowledging the importance of modal transition systems, we define a state/event based logic over a modified modal transition system as a precursor to further work.