The Complexity of Model-Checking Tail-Recursive Higher-Order Fixpoint Logic

2021 ◽  
Vol 178 (1-2) ◽  
pp. 1-30
Author(s):  
Florian Bruse ◽  
Martin Lange ◽  
Etienne Lozes
Keyword(s):  
Model Checking ◽  
Lower Bounds ◽  
Expressive Power ◽  
Higher Order ◽  
Order Logic ◽  
High Complexity ◽  
Transition Systems ◽  
Recursive Formulas ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed λ-calculus into the modal μ-calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most k < 0. In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in (k − 1)-EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.

scholarly journals Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

2021 ◽  
Vol 22 (2) ◽  
pp. 1-37
Author(s):  
Christopher H. Broadbent ◽  
Arnaud Carayol ◽  
C.-H. Luke Ong ◽  
Olivier Serre
Keyword(s):  
Model Checking ◽  
Free Variable ◽  
Higher Order ◽  
Second Order ◽  
Effective Solution ◽  
Parity Games ◽  
Transition Graphs ◽  
Second Order Logic ◽  
Pushdown Automata ◽  
Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

scholarly journals First order quantifiers in monadic second order logic

2004 ◽  
Vol 69 (1) ◽  
pp. 118-136 ◽  
Author(s):  
H. Jerome Keisler ◽  
Wafik Boulos Lotfallah
Keyword(s):  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
Existential Quantifier ◽  
Reachability Problem ◽  
Open Problems ◽  
First Order ◽  
Second Order Logic ◽  
Monadic Second Order Logic ◽  
Quantifier Alternation

AbstractThis paper studies the expressive power that an extra first order quantifier adds to a fragment of monadic second order logic, extending the toolkit of Janin and Marcinkowski [JM01].We introduce an operation existsn (S) on properties S that says “there are n components having S”. We use this operation to show that under natural strictness conditions, adding a first order quantifier word u to the beginning of a prefix class V increases the expressive power monotonically in u. As a corollary, if the first order quantifiers are not already absorbed in V, then both the quantifier alternation hierarchy and the existential quantifier hierarchy in the positive first order closure of V are strict.We generalize and simplify methods from Marcinkowski [Mar99] to uncover limitations of the expressive power of an additional first order quantifier, and show that for a wide class of properties S, S cannot belong to the positive first order closure of a monadic prefix class W unless it already belongs to W.We introduce another operation alt(S) on properties which has the same relationship with the Circuit Value Problem as reach(S) (defined in [JM01]) has with the Directed Reachability Problem. We use alt(S) to show that Πn ⊈ FO(Σn), Σn ⊈ FO(∆n). and ∆n+1 ⊈ FOB(Σn), solving some open problems raised in [Mat98].

scholarly journals Decidability of Model Checking Multi-Agent Systems with Regular Expressions against Epistemic HS Specifications

2019 ◽  
Author(s):  
Jakub Michaliszyn ◽  
Piotr Witkowski
Keyword(s):  
Model Checking ◽  
Temporal Logic ◽  
Order Logic ◽  
Regular Expressions ◽  
Multi Agent Systems ◽  
Agent Systems ◽  
Interval Temporal Logic ◽  
Multi Agent ◽  
Second Order Logic ◽  
Monadic Second Order Logic

Epistemic Halpern-Shoham logic (EHS) is an interval temporal logic defined to verify properties of Multi-Agent Systems. In this paper we show that the model checking Multi-Agent Systems with regular expressions against the EHS specifications is decidable. We achieve this by reducing the model checking problem to the satisfiability problem of Monadic Second-Order Logic on trees.

scholarly journals Monadic Second-Order Logic, Graphs and Unfoldings of Transition Systems

1995 ◽  
Vol 2 (44) ◽  
Author(s):  
Bruno Courcelle ◽  
Igor Walukiewicz
Keyword(s):  
Transition System ◽  
Second Order ◽  
Order Logic ◽  
Order Property ◽  
Transition Systems ◽  
Graph Coverings ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We prove that every monadic second-order property of the unfolding<br />of a transition system is a monadic second-order property of the<br />system itself. We prove a similar result for certain graph coverings.

scholarly journals Local Normal Forms for First-Order Logic with Applications to Games and Automata

1999 ◽  
Vol Vol. 3 no. 3 ◽  
Author(s):  
Thomas Schwentick ◽  
Klaus Barthelmann
Keyword(s):  
Normal Forms ◽  
Winning Strategy ◽  
Expressive Power ◽  
Second Order ◽  
Order Logic ◽  
First Order Logic ◽  
First Order ◽  
Relational Structures ◽  
Second Order Logic ◽  
Monadic Second Order Logic

International audience Building on work of Gaifman [Gai82] it is shown that every first-order formula is logically equivalent to a formula of the form ∃ x_1,...,x_l, \forall y, φ where φ is r-local around y, i.e. quantification in φ is restricted to elements of the universe of distance at most r from y. \par From this and related normal forms, variants of the Ehrenfeucht game for first-order and existential monadic second-order logic are developed that restrict the possible strategies for the spoiler, one of the two players. This makes proofs of the existence of a winning strategy for the duplicator, the other player, easier and can thus simplify inexpressibility proofs. \par As another application, automata models are defined that have, on arbitrary classes of relational structures, exactly the expressive power of first-order logic and existential monadic second-order logic, respectively.

scholarly journals Automated Logical Verification based on Trace Abstractions

1995 ◽  
Vol 2 (53) ◽  
Author(s):  
Nils Klarlund ◽  
Mogens Nielsen ◽  
Kim Sunesen
Keyword(s):  
Distributed Systems ◽  
Model Checking ◽  
State Space ◽  
Temporal Logic ◽  
Second Order ◽  
Order Logic ◽  
Verification Problem ◽  
Finite State ◽  
Second Order Logic ◽  
Monadic Second Order Logic

We propose a new and practical framework for integrating the behavioral<br />reasoning about distributed systems with model-checking methods.<br />Our proof methods are based on trace abstractions, which relate the<br />behaviors of the program and the specification. We show that for finite-state<br />systems such symbolic abstractions can be specified conveniently in<br />Monadic Second-Order Logic (M2L). Model-checking is then made possible<br />by the reduction of non-determinism implied by the trace abstraction.<br />Our method has been applied to a recent verification problem by Broy<br />and Lamport. We have transcribed their behavioral description of a distributed<br />program into temporal logic and verified it against another distributed<br />system without constructing the global program state space. The<br />reasoning is expressed entirely within M2L and is carried out by a decision<br />procedure. Thus M2L is a practical vehicle for handling complex temporal<br />logic specifications, where formulas decided by a push of a button are as<br />long as 10-15 pages.

scholarly journals A uniform method for proving lower bounds on the computational complexity of logical theories

2001 ◽  
Author(s):  
Kevin J. Compton ◽  
C. Ward Henson
Keyword(s):  
Computational Complexity ◽  
Lower Bounds ◽  
Uniform Method ◽  
Order Logic ◽  
First Order Logic ◽  
Finite Model ◽  
Relation Symbol ◽  
Unary Relation ◽  
Second Order Logic ◽  
Monadic Second Order Logic

In this chapter we present a method for obtaining lower bounds on the computational complexity of logical theories, and give several illustrations of its use. This method is an extension of widely used procedures for proving the recursive undecidability of logical theories. (See Rabin [1965] and Eršov et al. [1965].) One important aspect of this method is that it is based on a family of inseparability results for certain logical problems, closely related to the well-known inseparability result of Trakhtenbrot (as refined by Vaught), that no recursive set separates the logically valid sentences from those which are false in some finite model, as long as the underlying language has at least one non-unary relation symbol. By using these inseparability results as a foundation, we are able to obtain hereditary lower bounds, i.e., bounds which apply uniformly to all subtheories of the theory. The second important aspect of this method is that we use interpretations to transfer lower bounds from one theory to another. By doing this we eliminate the need to code machine computations into the models of the theory being studied. (The coding of computations is done once and for all in proving the inseparability results.) By using interpretations, attention is centred on much simpler definability considerations, viz., what kinds of binary relations on large finite sets can be defined using short formulas in models of the theory. This is conceptually much simpler than other approaches that have been proposed for obtaining lower bounds, such as the method of bounded concatenations of Fleischmann et al. [1977]. We will deal primarily with theories in first-order logic and monadic second-order logic.

Sign in / Sign up

Export Citation Format

Share Document