Showing 1–11 of 11 results for author: Mundhenk, M

The model checking fingerprints of CTL operators

Authors: Andreas Krebs, Arne Meier, Martin Mundhenk

Abstract: The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking. The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking. △ Less

Submitted 20 July, 2015; v1 submitted 18 April, 2015; originally announced April 2015.

The Complexity of Plan Existence and Evaluation in Probabilistic Domains

Authors: Judy Goldsmith, Michael L. Littman, Martin Mundhenk

Abstract: We examine the computational complexity of testing and finding small plans in probabilistic planning domains with succinct representations. We find that many problems of interest are complete for a variety of complexity classes: NP, co-NP, PP, NP^PP, co-NP^PP, and PSPACE. Of these, the probabilistic classes PP and NP^PP are likely to be of special interest in the field of uncertainty in artifici… ▽ More We examine the computational complexity of testing and finding small plans in probabilistic planning domains with succinct representations. We find that many problems of interest are complete for a variety of complexity classes: NP, co-NP, PP, NP^PP, co-NP^PP, and PSPACE. Of these, the probabilistic classes PP and NP^PP are likely to be of special interest in the field of uncertainty in artificial intelligence and are deserving of additional study. These results suggest a fruitful direction of future algorithmic development. △ Less

Submitted 6 February, 2013; originally announced February 2013.

Comments: Appears in Proceedings of the Thirteenth Conference on Uncertainty in Artificial Intelligence (UAI1997)

Report number: UAI-P-1997-PG-182-189

The Complexity of Monotone Hybrid Logics over Linear Frames and the Natural Numbers

Authors: Stefan Göller, Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Felix Weiss

Abstract: Hybrid logic with binders is an expressive specification language. Its satisfiability problem is undecidable in general. If frames are restricted to N or general linear orders, then satisfiability is known to be decidable, but of non-elementary complexity. In this paper, we consider monotone hybrid logics (i.e., the Boolean connectives are conjunction and disjunction only) over N and general linea… ▽ More Hybrid logic with binders is an expressive specification language. Its satisfiability problem is undecidable in general. If frames are restricted to N or general linear orders, then satisfiability is known to be decidable, but of non-elementary complexity. In this paper, we consider monotone hybrid logics (i.e., the Boolean connectives are conjunction and disjunction only) over N and general linear orders. We show that the satisfiability problem remains non-elementary over linear orders, but its complexity drops to PSPACE-completeness over N. We categorize the strict fragments arising from different combinations of modal and hybrid operators into NP-complete and tractable (i.e. complete for NC1or LOGSPACE). Interestingly, NP-completeness depends only on the fragment and not on the frame. For the cases above NP, satisfiability over linear orders is harder than over N, while below NP it is at most as hard. In addition we examine model-theoretic properties of the fragments in question. △ Less

Submitted 12 June, 2012; v1 submitted 5 April, 2012; originally announced April 2012.

Comments: 19 pages + 15 pages appendix, 3 figures

MSC Class: 03B45; 68Q17 ACM Class: F.2; F.4

Intuitionistic implication makes model checking hard

Authors: Martin Mundhenk, Felix Weiss

Abstract: We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. More specific, we consider intuitionistic logic IPC, basic propositional logic BPL, formal propositional logic FPL, and Jankov's logic KC. We show that the model checking problem is P-complete for the implicational fragments of all these intuitionistic logic… ▽ More We investigate the complexity of the model checking problem for intuitionistic and modal propositional logics over transitive Kripke models. More specific, we consider intuitionistic logic IPC, basic propositional logic BPL, formal propositional logic FPL, and Jankov's logic KC. We show that the model checking problem is P-complete for the implicational fragments of all these intuitionistic logics. For BPL and FPL we reach P-hardness even on the implicational fragment with only one variable. The same hardness results are obtained for the strictly implicational fragments of their modal companions. Moreover, we investigate whether formulas with less variables and additional connectives make model checking easier. Whereas for variable free formulas outside of the implicational fragment, FPL model checking is shown to be in LOGCFL, the problem remains P-complete for BPL. △ Less

Submitted 25 April, 2012; v1 submitted 11 July, 2011; originally announced July 2011.

Comments: 29 pages, 10 figures

ACM Class: 03B20, 68Q15, 68Q17

Journal ref: Logical Methods in Computer Science, Volume 8, Issue 2 (April 27, 2012) lmcs:1160

Nonapproximability Results for Partially Observable Markov Decision Processes

Authors: J. Goldsmith, C. Lusena, M. Mundhenk

Abstract: We show that for several variations of partially observable Markov decision processes, polynomial-time algorithms for finding control policies are unlikely to or simply don't have guarantees of finding policies within a constant factor or a constant summand of optimal. Here "unlikely" means "unless some complexity classes collapse," where the collapses considered are P=NP, P=PSPACE… ▽ More We show that for several variations of partially observable Markov decision processes, polynomial-time algorithms for finding control policies are unlikely to or simply don't have guarantees of finding policies within a constant factor or a constant summand of optimal. Here "unlikely" means "unless some complexity classes collapse," where the collapses considered are P=NP, P=PSPACE, or P=EXP. Until or unless these collapses are shown to hold, any control-policy designer must choose between such performance guarantees and efficient computation. △ Less

Submitted 1 June, 2011; originally announced June 2011.

Journal ref: Journal Of Artificial Intelligence Research, Volume 14, pages 83-103, 2001

Model Checking CTL is Almost Always Inherently Sequential

Authors: Olaf Beyersdorff, Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Heribert Vollmer

Abstract: The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) and Markey (2004). For all these fragments, except for the trivial case without any temporal operator… ▽ More The model checking problem for CTL is known to be P-complete (Clarke, Emerson, and Sistla (1986), see Schnoebelen (2002)). We consider fragments of CTL obtained by restricting the use of temporal modalities or the use of negations---restrictions already studied for LTL by Sistla and Clarke (1985) and Markey (2004). For all these fragments, except for the trivial case without any temporal operator, we systematically prove model checking to be either inherently sequential (P-complete) or very efficiently parallelizable (LOGCFL-complete). For most fragments, however, model checking for CTL is already P-complete. Hence our results indicate that, in cases where the combined complexity is of relevance, approaching CTL model checking by parallelism cannot be expected to result in any significant speedup. We also completely determine the complexity of the model checking problem for all fragments of the extensions ECTL, CTL+, and ECTL+. △ Less

Submitted 15 November, 2011; v1 submitted 25 March, 2011; originally announced March 2011.

ACM Class: cs.CC

Journal ref: Logical Methods in Computer Science, Volume 7, Issue 2 (May 17, 2011) lmcs:1007

The model checking problem for intuitionistic propositional logic with one variable is AC1-complete

Authors: Martin Mundhenk, Felix Weiss

Abstract: We show that the model checking problem for intuitionistic propositional logic with one variable is complete for logspace-uniform AC1. As basic tool we use the connection between intuitionistic logic and Heyting algebra, and investigate its complexity theoretical aspects. For superintuitionistic logics with one variable, we obtain NC1-completeness for the model checking problem. We show that the model checking problem for intuitionistic propositional logic with one variable is complete for logspace-uniform AC1. As basic tool we use the connection between intuitionistic logic and Heyting algebra, and investigate its complexity theoretical aspects. For superintuitionistic logics with one variable, we obtain NC1-completeness for the model checking problem. △ Less

Submitted 15 September, 2011; v1 submitted 17 December, 2010; originally announced December 2010.

Comments: A preliminary version of this work was presented at STACS 2011. 19 pages, 3 figures

MSC Class: 68Q17 (Primary); 03B20 (Secondary) ACM Class: F.2; F.4

The Complexity of Satisfiability for Fragments of Hybrid Logic -- Part I

Authors: Arne Meier, Martin Mundhenk, Thomas Schneider, Michael Thomas, Volker Weber, Felix Weiss

Abstract: The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equ… ▽ More The satisfiability problem of hybrid logics with the downarrow binder is known to be undecidable. This initiated a research program on decidable and tractable fragments. In this paper, we investigate the effect of restricting the propositional part of the language on decidability and on the complexity of the satisfiability problem over arbitrary, transitive, total frames, and frames based on equivalence relations. We also consider different sets of modal and hybrid operators. We trace the border of decidability and give the precise complexity of most fragments, in particular for all fragments including negation. For the monotone fragments, we are able to distinguish the easy from the hard cases, depending on the allowed set of operators. △ Less

Submitted 8 June, 2009; originally announced June 2009.

ACM Class: F.4.1

Complexity of Hybrid Logics over Transitive Frames

Authors: Martin Mundhenk, Thomas Schneider, Thomas Schwentick, Volker Weber

Abstract: This paper examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator is NEXPTIME-complete. This is in contrast to undecidability of satisfiability over arbitrary frames for this language (Areces, Blackburn, Marx 1999). It is also shown that a… ▽ More This paper examines the complexity of hybrid logics over transitive frames, transitive trees, and linear frames. We show that satisfiability over transitive frames for the hybrid language extended with the downarrow operator is NEXPTIME-complete. This is in contrast to undecidability of satisfiability over arbitrary frames for this language (Areces, Blackburn, Marx 1999). It is also shown that adding the @ operator or the past modality leads to undecidability over transitive frames. This is again in contrast to the case of transitive trees and linear frames, where we show these languages to be nonelementarily decidable. Moreover, we establish 2EXPTIME and EXPTIME upper bounds for satisfiability over transitive frames and transitive trees, respectively, for the hybrid Until/Since language. An EXPTIME lower bound is shown to hold for the modal Until language over both frame classes. △ Less

Submitted 25 June, 2008; originally announced June 2008.

Comments: 21 pages, 6 figures (only 2 thereof are in external files)

ACM Class: F.4.1

Journal ref: Workshop "Methods for Modalities" (M4M-4), Informatik-Berichte, 194, pp. 62-78, 2005. ISSN 0863-095X

The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments

Authors: Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

Abstract: In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper systematically studies the model-checking problem for LTL formulae over restricte… ▽ More In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper systematically studies the model-checking problem for LTL formulae over restricted sets of propositional and temporal operators. For almost all combinations of temporal and propositional operators, we determine whether the model-checking problem is tractable (in P) or intractable (NP-hard). We then focus on the tractable cases, showing that they all are NL-complete or even logspace solvable. This leads to a surprising gap in complexity between tractable and intractable cases. It is worth noting that our analysis covers an infinite set of problems, since there are infinitely many sets of propositional operators. △ Less

Submitted 5 May, 2008; originally announced May 2008.

Comments: 27 pages, 7 figures

Report number: ECCC Report TR08-028 ACM Class: F.4.1; I.2.4

The Computational Complexity of Probabilistic Planning

Authors: M. L. Littman, J. Goldsmith, M. Mundhenk

Abstract: We examine the computational complexity of testing and finding small plans in probabilistic planning domains with both flat and propositional representations. The complexity of plan evaluation and existence varies with the plan type sought; we examine totally ordered plans, acyclic plans, and looping plans, and partially ordered plans under three natural definitions of plan value. We show that p… ▽ More We examine the computational complexity of testing and finding small plans in probabilistic planning domains with both flat and propositional representations. The complexity of plan evaluation and existence varies with the plan type sought; we examine totally ordered plans, acyclic plans, and looping plans, and partially ordered plans under three natural definitions of plan value. We show that problems of interest are complete for a variety of complexity classes: PL, P, NP, co-NP, PP, NP^PP, co-NP^PP, and PSPACE. In the process of proving that certain planning problems are complete for NP^PP, we introduce a new basic NP^PP-complete problem, E-MAJSAT, which generalizes the standard Boolean satisfiability problem to computations involving probabilistic quantities; our results suggest that the development of good heuristics for E-MAJSAT could be important for the creation of efficient algorithms for a wide variety of problems. △ Less

Submitted 31 July, 1998; originally announced August 1998.

Comments: See http://www.jair.org/ for any accompanying files

Journal ref: Journal of Artificial Intelligence Research, Vol 9, (1998), 1-36