arXiv subjects

Laura Bozzelli

Publications and source records attributed to Laura Bozzelli.

29 records · Page 2Linked to original sources

arXiv2017

On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions

In this paper, we investigate the model checking (MC) problem for Halpern and Shoham's interval temporal logic HS. In the last years, interval temporal logic MC has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic MC, which can be recovered as a special case. Most results have been obtained under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over each component state. Recently, Lomuscio and Michaliszyn proposed a way to relax such an assumption by exploiting regular expressions to define the behaviour of proposition letters over intervals in terms of their component states. When homogeneity is assumed, the exact complexity of MC is a difficult open question for full HS and for its two syntactically maximal fragments AA'BB'E' and AA'EB'E'. In this paper, we provide an asymptotically optimal bound to the complexity of these two fragments under the more expressive semantic variant based on regular expressions by showing that their MC problem is AEXP_pol-complete, where AEXP_pol denotes the complexity class of problems decided by exponential-time bounded alternating Turing Machines making a polynomially bounded number of alternations.

cs.LO↗

arXiv2016

Model Checking the Logic of Allen's Relations Meets and Started-by is $P^NP$-Complete

In the plethora of fragments of Halpern and Shoham's modal logic of time intervals (HS), the logic AB of Allen's relations Meets and Started-by is at a central position. Statements that may be true at certain intervals, but at no sub-interval of them, such as accomplishments, as well as metric constraints about the length of intervals, that force, for instance, an interval to be at least (resp., at most, exactly) k points long, can be expressed in AB. Moreover, over the linear order of the natural numbers N, it subsumes the (point-based) logic LTL, as it can easily encode the next and until modalities. Finally, it is expressive enough to capture the ω-regular languages, that is, for each ω-regular expression R there exists an AB formula ϕ such that the language defined by R coincides with the set of models of ϕ over N. It has been shown that the satisfiability problem for AB over N is EXPSPACE-complete. Here we prove that, under the homogeneity assumption, its model checking problem is Δ^p_2 = P^NP-complete (for the sake of comparison, the model checking problem for full HS is EXPSPACE-hard, and the only known decision procedure is nonelementary). Moreover, we show that the modality for the Allen relation Met-by can be added to AB at no extra cost (AA'B is P^NP-complete as well).

cs.LO↗

arXiv2015

On the complexity of Temporal Equilibrium Logic

Temporal Equilibrium Logic (TEL) is a promising framework that extends the knowledge representation and reasoning capabilities of Answer Set Programming with temporal operators in the style of LTL. To our knowledge it is the first nonmonotonic logic that accommodates fully the syntax of a standard temporal logic (specifically LTL) without requiring further constructions. This paper provides a systematic complexity analysis for the (consistency) problem of checking the existence of a temporal equilibrium model of a TEL formula. It was previously shown that this problem in the general case lies somewhere between PSPACE and EXPSPACE. Here we establish a lower bound matching the known EXPSPACE upper bound. Additionally we analyse the complexity for various natural subclasses of TEL formulas, identifying both tractable and intractable fragments. Finally the paper offers some new insights on the logic LTL by addressing satisfiability for minimal LTL models. The complexity results obtained highlight a substantial difference between interpreting LTL over finite or infinite words.

cs.LO↗

arXiv2014

Unifying Hyper and Epistemic Temporal Logic

In the literature, two powerful temporal logic formalisms have been proposed for expressing information flow security requirements, that in general, go beyond regular properties. One is classic, based on the knowledge modalities of epistemic logic. The other one, the so called hyper logic, is more recent and subsumes many proposals from the literature; it is based on explicit and simultaneous quantification over multiple paths. In an attempt to better understand how these logics compare with each other, we consider the logic KCTL* (the extension of CTL* with knowledge modalities and synchronous perfect recall semantics) and HyperCTL*. We first establish that KCTL* and HyperCTL* are expressively incomparable. Second, we introduce and study a natural linear past extension of HyperCTL* to unify KCTL* and HyperCTL*; indeed, we show that KCTL* can be easily translated in linear time into the proposed logic. Moreover, we show that the model-checking problem for this novel logic is decidable, and we provide its exact computational complexity in terms of a new measure of path quantifiers' alternation. For this, we settle open complexity issues for unrestricted quantified propositional temporal logic.

cs.LO↗

arXiv2013

Refinement Modal Logic

In this paper we present {\em refinement modal logic}. A refinement is like a bisimulation, except that from the three relational requirements only `atoms' and `back' need to be satisfied. Our logic contains a new operator 'all' in addition to the standard modalities 'box' for each agent. The operator 'all' acts as a quantifier over the set of all refinements of a given model. As a variation on a bisimulation quantifier, this refinement operator or refinement quantifier 'all' can be seen as quantifying over a variable not occurring in the formula bound by it. The logic combines the simplicity of multi-agent modal logic with some powers of monadic second-order quantification. We present a sound and complete axiomatization of multi-agent refinement modal logic. We also present an extension of the logic to the modal mu-calculus, and an axiomatization for the single-agent version of this logic. Examples and applications are also discussed: to software verification and design (the set of agents can also be seen as a set of actions), and to dynamic epistemic logic. We further give detailed results on the complexity of satisfiability, and on succinctness.

cs.LO↗

arXiv2013

The Complexity of Synthesizing Uniform Strategies

We investigate uniformity properties of strategies. These properties involve sets of plays in order to express useful constraints on strategies that are not μ-calculus definable. Typically, we can state that a strategy is observation-based. We propose a formal language to specify uniformity properties, interpreted over two-player turn-based arenas equipped with a binary relation between plays. This way, we capture e.g. games with winning conditions expressible in epistemic temporal logic, whose underlying equivalence relation between plays reflects the observational capabilities of agents (for example, synchronous perfect recall). Our framework naturally generalizes many other situations from the literature. We establish that the problem of synthesizing strategies under uniformity constraints based on regular binary relations between plays is non-elementary complete.

cs.GT↗

arXiv2011

New results on pushdown module checking with imperfect information

Model checking of open pushdown systems (OPD) w.r.t. standard branching temporal logics (pushdown module checking or PMC) has been recently investigated in the literature, both in the context of environments with perfect and imperfect information about the system (in the last case, the environment has only a partial view of the system's control states and stack content). For standard CTL, PMC with imperfect information is known to be undecidable. If the stack content is assumed to be visible, then the problem is decidable and 2EXPTIME-complete (matching the complexity of PMC with perfect information against CTL). The decidability status of PMC with imperfect information against CTL restricted to the case where the depth of the stack content is visible is open. In this paper, we show that with this restriction, PMC with imperfect information against CTL remains undecidable. On the other hand, we individuate an interesting subclass of OPDS with visible stack content depth such that PMC with imperfect information against the existential fragment of CTL is decidable and in 2EXPTIME. Moreover, we show that the program complexity of PMC with imperfect information and visible stack content against CTL is 2EXPTIME-complete (hence, exponentially harder than the program complexity of PMC with perfect information, which is known to be EXPTIME-complete).

cs.LO↗

arXiv2011

Opacity Issues in Games with Imperfect Information

We study in depth the class of games with opacity condition, which are two-player games with imperfect information in which one of the players only has imperfect information, and where the winning condition relies on the information he has along the play. Those games are relevant for security aspects of computing systems: a play is opaque whenever the player who has imperfect information never "knows" for sure that the current position is one of the distinguished "secret" positions. We study the problems of deciding the existence of a winning strategy for each player, and we call them the opacity-violate problem and the opacity-guarantee problem. Focusing on the player with perfect information is new in the field of games with imperfect-information because when considering classical winning conditions it amounts to solving the underlying perfect-information game. We establish the EXPTIME-completeness of both above-mentioned problems, showing that our winning condition brings a gap of complexity for the player with perfect information, and we exhibit the relevant opacity-verify problem, which noticeably generalizes approaches considered in the literature for opacity analysis in discrete-event systems. In the case of blindfold games, this problem relates to the two initial ones, yielding the determinacy of blindfold games with opacity condition and the PSPACE-completeness of the three problems.

cs.GT↗

arXiv2004

Model checking for Process Rewrite Systems and a class of action--based regular properties

We consider the model checking problem for Process Rewrite Systems (PRSs), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRSs can be adopted as formal models for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem for PRSs and action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRSs. As a consequence, we obtain decidability of the model-checking (restricted to infinite runs) for PRSs and a meaningful fragment of ALTL.

cs.OH↗

arXiv2004

Verification of Process Rewrite Systems in normal form

We consider the problem of model--checking for Process Rewrite Systems (PRSs) in normal form. In a PRS in normal form every rewrite rule either only deals with procedure calls and procedure termination, possibly with value return, (this kind of rules allows to capture Pushdown Processes), or only deals with dynamic activation of processes and synchronization (this kind of rules allows to capture Petri Nets). The model-checking problem for PRSs and action-based linear temporal logic (ALTL) is undecidable. However, decidability of model--checking for PRSs and some interesting fragment of ALTL remains an open question. In this paper we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewritings) in PRSs in normal form. As a consequence, we obtain decidability of the model-checking (restricted to infinite runs) for PRSs in normal form and a meaningful fragment of ALTL.

cs.OH↗

arXiv2003

Verification of recursive parallel systems

In this paper we consider the problem of proving properties of infinite behaviour of formalisms suitable to describe (infinite state) systems with recursion and parallelism. As a formal setting, we consider the framework of Process Rewriting Systems (PRSs). For a meaningfull fragment of PRSs, allowing to accommodate both Pushdown Automata and Petri Nets, we state decidability results for a class of properties about infinite derivations (infinite term rewritings). The given results can be exploited for the automatic verification of some classes of linear time properties of infinite state systems described by PRSs. In order to exemplify the assessed results, we introduce a meaningful automaton based formalism which allows to express both recursion and multi--treading.

cs.LO↗