Hybrid Branching-Time Logics - Computer Science > Logic in Computer ScienceReportar como inadecuado




Hybrid Branching-Time Logics - Computer Science > Logic in Computer Science - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

Abstract: Hybrid branching-time logics are introduced as extensions of CTL-like logicswith state variables and the downarrow-binder. Following recent work in thelinear framework, only logics with a single variable are considered. Theexpressive power and the complexity of satisfiability of the resulting logicsis investigated.As main result, the satisfiability problem for the hybrid versions of severalbranching-time logics is proved to be 2EXPTIME-complete. These branching-timelogics range from strict fragments of CTL to extensions of CTL that can talkabout the past and express fairness-properties. The complexity gap relative toCTL is explained by a corresponding succinctness result.To prove the upper bound, the automata-theoretic approach to branching-timelogics is extended to hybrid logics, showing that non-emptiness of alternatingone-pebble Buchi tree automata is 2EXPTIME-complete.



Autor: Volker Weber

Fuente: https://arxiv.org/







Documentos relacionados