Branching-Time Logics Repeatedly Referring to States |
| |
Authors: | Volker Weber |
| |
Affiliation: | 1. Fakult?t für Informatik, Technische Universit?t Dortmund, 44221, Dortmund, Germany
|
| |
Abstract: | While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics
able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism,
hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning
a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem.
As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics.
As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be
2EXPTIME-complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The
ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability
for NCTL* has nonelementary complexity. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|