scholarly journals Uniform Satisfiability Problem for Local Temporal Logics over Mazurkiewicz Traces

2005 ◽  
pp. 533-547 ◽  
Author(s):  
Paul Gastin ◽  
Dietrich Kuske
Keyword(s):  
Satisfiability Problem ◽  
Temporal Logics ◽  
Mazurkiewicz Traces

scholarly journals The power of modal separation logics

2019 ◽  
Vol 29 (8) ◽  
pp. 1139-1184 ◽  
Author(s):  
Stéphane Demri ◽  
Raul Fervari
Keyword(s):  
Separation Logic ◽  
Satisfiability Problem ◽  
Alternative Semantics ◽  
Temporal Logics ◽  
Original Language ◽  
Modal Operators ◽  
Logical Connectives ◽  
Np Complete ◽  
Memory States ◽  
The Difference

Abstract We introduce a modal separation logic MSL whose models are memory states from separation logic and the logical connectives include modal operators as well as separating conjunction and implication from separation logic. With such a combination of operators, some fragments of MSL can be seen as genuine modal logics whereas some others capture standard separation logics, leading to an original language to speak about memory states. We analyse the decidability status and the computational complexity of several fragments of MSL, obtaining surprising results by design of proof methods that take into account the modal and separation features of MSL. For example, the satisfiability problem for the fragment of MSL with $\Diamond $, the difference modality $\langle \neq \rangle $ and separating conjunction $\ast $ is shown Tower-complete whereas the restriction either to $\Diamond $ and $\ast $ or to $\langle \neq \rangle $ and $\ast $ is only NP-complete. We establish that the full logic MSL admits an undecidable satisfiability problem. Furthermore, we investigate variants of MSL with alternative semantics and we build bridges with interval temporal logics and with logics equipped with sabotage operators.

scholarly journals From local to global temporal logics over Mazurkiewicz traces

2006 ◽  
Vol 356 (1-2) ◽  
pp. 126-135 ◽  
Author(s):  
Volker Diekert ◽  
Paul Gastin
Keyword(s):  
Temporal Logics ◽  
Mazurkiewicz Traces

scholarly journals On Coarser Interval Temporal Logics and their Satisfiability Problem

2015 ◽  
pp. 105-115 ◽  
Author(s):  
Emilio Muñoz-Velasco ◽  
Mercedes Pelegrín-García ◽  
Pietro Sala ◽  
Guido Sciavicco
Keyword(s):  
Satisfiability Problem ◽  
Temporal Logics ◽  
Interval Temporal Logics

scholarly journals Combining DL-Lite_{bool}^N with Branching Time: A gentle Marriage

2017 ◽  
Author(s):  
Víctor Gutiérrez-Basulto ◽  
Jean Christoph Jung
Keyword(s):  
Description Logic ◽  
Satisfiability Problem ◽  
Branching Time ◽  
Temporal Logics ◽  
Complexity Bounds

We study combinations of the description logic DL-Lite_{bool}^N with the branching temporal logics CTL* and CTL. We analyse two types of combinations, both with rigid roles: (i) temporal operators are applied to concepts and to ABox assertions, and (ii) temporal operators are applied to concepts and Boolean combinations of concept inclusions and ABox assertions. For the resulting logics, we present algorithms for the satisfiability problem and (mostly tight) complexity bounds ranging from ExpTime to 3ExpTime.

Sign in / Sign up

Export Citation Format

Share Document