In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening proof of the selection problem originally established by Carayol and Serre using collapsible pushdown automata. The main idea is to start from an infinitary and colored relational semantics of the lambdaY-calculus already formulated, and to replace it by its finitary counterpart based on finite prime-algebraic lattices. Given a higher-order recursion scheme G, the finiteness of its interpretation in the model enables us to associate to any MSO formula phi a new higher-order recursion scheme G_phi resolving the selection problem.
In the standard sequent presentations of Girard's Linear Logic (LL), there are two "non-decreasing" rules, where the premises are not smaller than the conclusion, namely the cut and the contraction rules. It is a universal concern to eliminate the cut rule. We show that, using an admissible modification of the tensor rule, contractions can be eliminated, and that cuts can be simultaneously limited to a single initial occurrence. This view leads to a consistent, but incomplete game model for LL with exponentials, which is finitary, in the sense that each play is finite. The game is based on a s…
We give a definition of finitary type theories that subsumes many examples of dependent type theories, such as variants of Martin-Löf type theory, simple type theories, first-order and higher-order logics, and homotopy type theory. We prove several general meta-theorems about finitary type theories: weakening, admissibility of substitution and instantiation of metavariables, derivability of presuppositions, uniqueness of typing, and inversion principles. We then give a second formulation of finitary type theories in which there are no explicit contexts. Instead, free variables are explicitly a…
This paper outlines new paradigms for real analysis and computability theory in the recently proposed non-Aristotelian finitary logic (NAFL). Constructive real analysis in NAFL (NRA) is accomplished by a translation of diagrammatic concepts from Euclidean geometry into an extension (NPAR) of the NAFL version of Peano Arithmetic (NPA). Such a translation is possible because NPA proves the existence of every infinite proper class of natural numbers that is definable in the language of NPA. Infinite sets are not permitted in NPAR and quantification over proper classes is banned; hence Cantor's di…
A weakly complete finitary axiomatization for EQPL (exogenous quantum propositional logic) is presented. The proof is carried out using a non trivial extension of the Fagin-Halpern-Megiddo technique together with three Henkin style completions.
This article surveys some of the recent work in verification of temporal epistemic logic via symbolic model checking, focusing on OBDD-based and SAT-based approaches for epistemic logics built on discrete and real-time branching time temporal logics.
We study the finitary satisfiability problem for first order logic with two variables and two binary relations, corresponding to the induced successor relations of two finite linear orders. We show that the problem is decidable in NEXPTIME.
Coalgebras for a functor model different types of transition systems in a uniform way. This paper focuses on a uniform account of finitary logics for set-based coalgebras. In particular, a general construction of a logic from an arbitrary set-functor is given and proven to be strongly complete under additional assumptions. We proceed in three parts. Part I argues that sifted colimit preserving functors are those functors that preserve universal algebraic structure. Our main theorem here states that a functor preserves sifted colimits if and only if it has a finitary presentation by operations …
We give the first ExpTime (complexity-optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHIQ when numbers are coded in unary. Our procedure is based on global state caching and integer linear feasibility checking.
We study generalized possibilistic computation tree logic model checking in this paper, which is an extension of possibilistic computation logic model checking introduced by Y.Li, Y.Li and Z.Ma (2014). The system is modeled by generalized possibilistic Kripke structures (GPKS, in short), and the verifying property is specified by a generalized possibilistic computation tree logic (GPoCTL, in short) formula. Based on generalized possibility measures and generalized necessity measures, the method of generalized possibilistic computation tree logic model checking is discussed, and the correspondi…
The molecular computing has been successfully employed to solve more and more complex computation problems. However, as an important complex problem, the model checking are still far from fully resolved under the circumstance of molecular computing, since it is still a lack of method. To address this issue, a model checking method is presented for checking the basic constructs in a given temporal logic using molecular computing. Through the design of the new encoding and calling this process, we get a molecule-based approach for checking all of the basic constructs of this logic.
Path checking, the special case of the model checking problem where the model under consideration is a single path, plays an important role in monitoring, testing, and verification. We prove that for linear-time temporal logic (LTL), path checking can be efficiently parallelized. In addition to the core logic, we consider the extensions of LTL with bounded-future (BLTL) and past-time (LTL+Past) operators. Even though both extensions improve the succinctness of the logic exponentially, path checking remains efficiently parallelizable: Our algorithm for LTL, LTL+Past, and BLTL+Past is in AC^1(lo…
Propositional and modal inclusion logic are formalisms that belong to the family of logics based on team semantics. This article investigates the model checking and validity problems of these logics. We identify complexity bounds for both problems, covering both lax and strict team semantics. By doing so, we come close to finalising the programme that ultimately aims to classify the complexities of the central reasoning problems for modal and propositional dependence, independence, and inclusion logics.
We study the computational complexity of model checking and satisfiability problems of polyadic modal logics extended with permutations and Boolean operators on accessibility relations. First, we show that the combined complexity of the model checking problem for the resulting logic is PTime-complete. Secondly, we show that the satisfiability problem of polyadic modal logic extended with negation on accessibility relations is ExpTime-complete. Finally, we show that the satisfiability problem of polyadic modal logic with permutations and Boolean operators on accessibility relations is ExpTime-c…
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded in the relational semantics of linear logic, the Church encoding of any higher-order recursion scheme (HORS) comes together with a dual Church encoding of an alternating tree automata (ATA) of the same signature. Moreover, the interaction between the relational interpretations of the HORS and of the ATA identifies the set of accepting states of the tree automaton against the infinite tree generated by the recursion s…
We give the first cut-free ExpTime (optimal) tableau decision procedure for checking satisfiability of a knowledge base in the description logic SHI, which extends the description logic ALC with transitive roles, inverse roles and role hierarchies.
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.
Given a formula in a temporal logic such as LTL or MTL, a fundamental problem is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC. In this paper, we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an NCC algorithm for UTL, the unary fragment of LTL. At the time of writing, MTL is the most expressive logic with an NC path-checking algorithm, and UTL is the most expressive fragment of LTL with a more efficient path-checking algorithm than for full LTL (subject to standard co…
Hybrid Spatiotemporal Logic for Automotive Applications: Modeling and Model-Checking
TU Wien（维也纳工业大学）；National Institute of Advanced Industrial Science and Technology (AIST)（国立产业技术综合研究所）；National Institute of Informatics (NII)（国立情报学研究所）
We study several extensions of linear-time and computation-tree temporal logics with quantifiers that allow for counting how often certain properties hold. For most of these extensions, the model-checking problem is undecidable, but we show that decidability can be recovered by considering flat Kripke structures where each state belongs to at most one simple loop. Most decision procedures are based on results on (flat) counter systems where counters are used to implement the evaluation of counting operators.
We consider quantitative extensions of the alternating-time temporal logics ATL/ATLs called quantitative alternating-time temporal logics (QATL/QATLs) in which the value of a counter can be compared to constants using equality, inequality and modulo constraints. We interpret these logics in one-counter game models which are infinite duration games played on finite control graphs where each transition can increase or decrease the value of an unbounded counter. That is, the state-space of these games are, generally, infinite. We consider the model-checking problem of the logics QATL and QATLs on…
The Epistemic Halpern-Shoham logic (EHS) is a temporal-epistemic logic that combines the interval operators of the Halpern-Shoham logic with epistemic modalities. The semantics of EHS is based on interpreted systems whose labelling function is defined on the endpoints of intervals. We show that this definition can be generalised by allowing the labelling function to be based on the whole interval by means of regular expressions. We prove that all the positive results known for EHS, notably the attractive complexity of its model checking problem for some of its fragments, still hold for its gen…
We investigate the decidability of model-checking logics of time, knowledge and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observed discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular,…
I consider the following generic scenario: an abstract model M of some 'real' system is only partially presented, or partially known to us, and we have to ensure that the actual system satisfies a given specification, formalised in some logical language. This scenario has at least two essentially different interpretations, leading to two, essentially different, formal logical and algorithmic problems: "Model Synthesis from Partial Models", where some 'admissible' extension of M to a full model must satisfy the specification, and "Model Checking of Partial Models", where all 'admissible' extens…
In this paper we investigate an extended version of modal dependence logic by allowing arbitrary Boolean connectives. Modal dependence logic was recently introduced by Jouko Väänänen by extending modal logic by a the dependence atom dep(.). In this paper we study the computational complexity of the model checking problem. For a complete classification of arbitrary Boolean functions we are using a Lattice approach introduced by Emil Post. This classification is done for all fragments of the logical language allowing modalities $\Diamond$ and $\Box$, the dependence atom, and logical symbols for …
We introduce the class of rational Kripke models and study symbolic model checking of the basic tense logic Kt and some extensions of it in models from that class. Rational Kripke models are based on (generally infinite) rational graphs, with vertices labeled by the words in some regular language and transitions recognized by asynchronous two-head finite automata, also known as rational transducers. Every atomic proposition in a rational Kripke model is evaluated in a regular set of states. We show that every formula of Kt has an effectively computable regular extension in every rational Kripk…
We study complexity of the model-checking problems for LTL with registers (also known as freeze LTL) and for first-order logic with data equality tests over one-counter automata. We consider several classes of one-counter automata (mainly deterministic vs. nondeterministic) and several logical fragments (restriction on the number of registers or variables and on the use of propositional variables for control locations). The logics have the ability to store a counter value and to test it later against the current counter value. We show that model checking over deterministic one-counter automata…
Propositional Projection Temporal Logic (PPTL) is a useful formalism for reasoning about period of time in hardware and software systems and can handle both sequential and parallel compositions. In this paper, based on discrete time Markov chains, we investigate the probabilistic model checking approach for PPTL towards verifying arbitrary linear-time properties. We first define a normal form graph, denoted by NFG_inf, to capture the infinite paths of PPTL formulas. Then we present an algorithm to generate the NFG_inf. Since discrete-time Markov chains are the deterministic probabilistic model…
While reasoning in a logic extending a complete Boolean basis is coNP-hard, restricting to conjunctive fragments of modal languages sometimes allows for tractable reasoning even in the presence of greatest fixpoints. One such example is the EL family of description logics; here, efficient reasoning is based on satisfaction checking in suitable small models that characterize formulas in terms of simulations. It is well-known, though, that not every conjunctive modal language has a tractable reasoning problem. Natural questions are then how common such tractable fragments are and how to identify…
We investigate the decidability of model-checking logics of time, knowledge and probability, with respect to two epistemic semantics: the clock and synchronous perfect recall semantics in partially observed discrete-time Markov chains. Decidability results are known for certain restricted logics with respect to these semantics, subject to a variety of restrictions that are either unexplained or involve a longstanding unsolved mathematical problem. We show that mild generalizations of the known decidable cases suffice to render the model checking problem definitively undecidable. In particular,…
The entailment between separation logic formulae with inductive predicates, also known as symbolic heaps, has been shown to be decidable for a large class of inductive definitions. Recently, a 2-EXPTIME algorithm was proposed and an EXPTIME-hard bound was established; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines.
In recent work, Kobayashi observed that the acceptance by an alternating tree automaton A of an infinite tree T generated by a higher-order recursion scheme G may be formulated as the typability of the recursion scheme G in an appropriate intersection type system associated to the automaton A. The purpose of this article is to establish a clean connection between this line of work and Bucciarelli and Ehrhard's indexed linear logic. This is achieved in two steps. First, we recast Kobayashi's result in an equivalent infinitary intersection type system where intersection is not idempotent anymore…
Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we s…
In the last decades much research effort has been devoted to extending the success of model checking from the traditional field of finite state machines and various versions of temporal logics to suitable subclasses of context-free languages and appropriate extensions of temporal logics. To the best of our knowledge such attempts only covered structured languages, i.e. languages whose structure is immediately "visible" in their sentences, such as tree-languages or visibly pushdown ones. In this paper we present a new temporal logic suitable to express and automatically verify properties of ope…
In order to deal with the systematic verification with uncertain infromation in possibility theory, Li and Li \cite{li12} introduced model checking of linear-time properties in which the uncertainty is modeled by possibility measures. Xue, Lei and Li \cite{Xue09} defined computation tree logic (CTL) based on possibility measures, which is called possibilistic CTL (PoCTL). This paper is a continuation of the above work. First, we study the expressiveness of PoCTL. Unlike probabilistic CTL, it is shown that PoCTL (in particular, qualitative PoCTL) is more powerful than CTL with respect to their …
Generalized Probabilistic Logic (GPL) is a temporal logic, based on the modal mu-calculus, for specifying properties of reactive probabilistic systems. We explore XPL, an extension to GPL allowing the semantics of nondeterminism present in Markov decision processes (MDPs). XPL is expressive enough that a number of independently studied problems--- such as termination of Recursive MDPs (RMDPs), PCTL* model checking of MDPs, and reachability for Branching MDPs--- can all be cast as model checking over XPL. Termination of multi-exit RMDPs is undecidable; thus, model checking in XPL is undecidable…
We develop a doubly-exponential decision procedure for the satisfiability problem of guarded separation logic -- a novel fragment of separation logic featuring user-supplied inductive predicates, Boolean connectives, and separating connectives, including restricted (guarded) versions of negation, magic wand, and septraction. Moreover, we show that dropping the guards for any of the above connectives leads to an undecidable fragment. We further apply our decision procedure to reason about entailments in the popular symbolic heap fragment of separation logic. In particular, we obtain a doubly-ex…
We introduce a new framework for Equivalence Checking (EC) of Boolean circuits based on a general technique called Logic Relaxation (LoR). The essence of LoR is to relax the formula to be solved and compute a superset S of the set of new behaviors. Namely, S contains all new satisfying assignments that appeared due to relaxation and does not contain assignments satisfying the original formula. Set S is generated by a procedure called partial quantifier elimination. If all possible bad behaviors are in S, the original formula cannot have them and so the property described by this formula holds.…
The unification problem in a propositional logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. When a unifiable formula has minimal complete sets of unifiers, the formula is either infinitary, finitary, or unitary, depending on the cardinality of its minimal complete sets of unifiers. In this paper, we study the unification types of some modal logics determined by classes of deterministic frames.
Gödel logic with the projection operator Delta (G_Delta) is an important many-valued as well as intermediate logic. In contrast to classical logic, the validity and the satisfiability problems of G_Delta are not directly dual to each other. We nevertheless provide a uniform, computational treatment of both problems for prenex formulas by describing appropriate translations into sets of order clauses that can be subjected to chaining resolution. For validity a version of Herbrand's Theorem allows us to show the soundness of standard Skolemization. For satisfiability the translation involves a n…
This volume contains the proceedings of the First Workshop on Logics and Model-checking for self-* systems (MOD* 2014). The worshop took place in Bertinoro, Italy, on 12th of September 2014, and was a satellite event of iFM 2014 (the 11th International Conference on Integrated Formal Methods). The workshop focuses on demonstrating the applicability of Formal Methods on modern complex systems with a high degree of self-adaptivity and reconfigurability, by bringing together researchers and practitioners with the goal of pushing forward the state of the art on logics and model checking.
Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) are often used to describe specifications of probabilistic properties for discrete time and continuous time, respectively. In PCTL and CSL, the possibility of executions satisfying some temporal properties can be quantitatively represented by the probabilistic extension of the path quantifiers in their basic Computation Tree Logic (CTL), however, path formulae of them are expressed via the same operators in CTL. For this reason, both of them cannot represent formulae with quantitative temporal properties, such as…
We study the complexity of the model checking problem, for fixed model A, over certain fragments L of first-order logic. These are sometimes known as the expression complexities of L. We obtain various complexity classification theorems for these logics L as each ranges over models A, in the spirit of the dichotomy conjecture for the Constraint Satisfaction Problem -- which itself may be seen as the model checking problem for existential conjunctive positive first-order logic.
Spatial aspects of computation are becoming increasingly relevant in Computer Science, especially in the field of collective adaptive systems and when dealing with systems distributed in physical space. Traditional formal verification techniques are well suited to analyse the temporal evolution of programs; however, properties of space are typically not taken into account explicitly. We present a topology-based approach to formal verification of spatial properties depending upon physical space. We define an appropriate logic, stemming from the tradition of topological interpretations of modal …
We present a formulation of the problem of probabilistic model checking as one of query evaluation over probabilistic logic programs. To the best of our knowledge, our formulation is the first of its kind, and it covers a rich class of probabilistic models and probabilistic temporal logics. The inference algorithms of existing probabilistic logic-programming systems are well defined only for queries with a finite number of explanations. This restriction prohibits the encoding of probabilistic model checkers, where explanations correspond to executions of the system being model checked. To over…
Model checking and automated theorem proving are two pillars of formal methods. This paper investigates model checking from an automated theorem proving perspective, aiming at combining the expressiveness of automated theorem proving and the complete automaticity of model checking. The focus of this paper is on the verification of temporal logic properties of Kripke models. The main contributions of this paper are: first the definition of an extended computation tree logic that allows polyadic predicate symbols, then a proof system for this logic, taking Kripke models as parameters, then, the …
We present a variant of ATL with distributed knowledge operators based on a synchronous and perfect recall semantics. The coalition modalities in this logic are based on partial observation of the full history, and incorporate a form of cooperation between members of the coalition in which agents issue their actions based on the distributed knowledge, for that coalition, of the system history. We show that model-checking is decidable for this logic. The technique utilizes two variants of games with imperfect information and partially observable objectives, as well as a subset construction for …
We study the first-order model checking problem on two generalisations of pushdown graphs. The first class is the class of nested pushdown trees. The other is the class of collapsible pushdown graphs. Our main results are the following. First-order logic with reachability is uniformly decidable on nested pushdown trees. Considering first-order logic without reachability, we prove decidability in doubly exponential alternating time with linearly many alternations. First-order logic with regular reachability predicates is uniformly decidable on level 2 collapsible pushdown graphs. Moreover, nest…
Live sequence charts (LSCs) have been proposed as an inter-object scenario-based specification and visual programming language for reactive systems. In this paper, we introduce a logic-based framework to check the consistency of an LSC specification. An LSC simulator has been implemented in logic programming, utilizing a memoized depth-first search strategy, to show how a reactive system in LSCs would response to a set of external event sequences. A formal notation is defined to specify external event sequences, extending the regular expression with a parallel operator and a testing control. T…
