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.
翻译:尽管纯动作或状态逻辑的研究更为广泛,但基于状态/事件的逻辑正变得日益重要。某些系统最适合通过同时包含状态和转移信息的结构进行研究,而正是这些结构构成了定义状态/事件逻辑的基础。UCTL逻辑及其变体或许是此类逻辑中迄今为止研究最为深入且实现最为广泛的体系。然而,目前尚未有学者定义UCTL*——这虽看似微不足道却具有研究价值的步骤。本文不仅完成了这项定义工作,更在UCTL与UCTL*两种情形下证明:这些逻辑的表达能力并不优于其更常见的片段。此外,鉴于模态转移系统的重要性,我们还在改进后的模态转移系统上定义了一种基于状态/事件的逻辑,作为后续研究的先导工作。