7 found
Sort by:
  1. Stefan Göller, Markus Lohrey & Carsten Lutz (2009). PDL with Intersection and Converse: Satisfiability and Infinite-State Model Checking. Journal of Symbolic Logic 74 (1):279-314.
    We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  2. Martin Lange & Carsten Lutz (2005). 2-ExpTime Lower Bounds for Propositional Dynamic Logics with Intersection. Journal of Symbolic Logic 70 (4):1072-1086.
    In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen (...)
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  3. Carsten Lutz & Dirk Walther (2005). PDL with Negation of Atomic Programs. Journal of Applied Non-Classical Logics 15 (2):189-213.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  4. Alessandro Artale & Carsten Lutz (2004). A Correspondence Between Temporal Description Logics. Journal of Applied Non-Classical Logics 14 (1-2):209-233.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  5. Roman Kontchakov, Carsten Lutz, Frank Wolter & Michael Zakharyaschev (2004). Temporalising Tableaux. Studia Logica 76 (1):91 - 134.
    As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  6. Carsten Lutz, Holger Sturm, Frank Wolter & Michael Zakharyaschev (2002). A Tableau Decision Algorithm for Modalized ALC with Constant Domains. Studia Logica 72 (2):199-232.
    The aim of this paper is to construct a tableau decision algorithm for the modal description logic K ALC with constant domains. More precisely, we present a tableau procedure that is capable of deciding, given an ALC-formula with extra modal operators (which are applied only to concepts and TBox axioms, but not to roles), whether is satisfiable in a model with constant domains and arbitrary accessibility relations. Tableau-based algorithms have been shown to be practical even for logics of rather high (...)
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  7. P. H. Rodenburg & Carsten Lutz (2001). A Complete System of Four-Valued Logic. Journal of Applied Non-Classical Logics 11 (3-4):367-392.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation