Hyperproperties are a modern specification paradigm that extends properties of a single trace to express properties of a set of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this article, we introduce two asynchronous and orthogonal extensions of HyperLTL, Stuttering HyperLTL (HyperLTL \({}_{S}\) ) and Context HyperLTL (HyperLTL \({}_{C}\) ). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking problem that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTL \({}_{S}\) fragment, coincides with that of the strictly less expressive logic HyperLTL.

Multi-Agent Systems (MAS) are essential for modelling strategic interactions between multiple agents, often involving partial information. Managing this partial information is crucial for accurate decision-making and strategy optimization. However, partial information combined with perfect recall strategies renders verifying strategic properties undecidable. Intuitionism, a form of partial information which has not yet been explored in the context of MAS, introduces a novel perspective. In this paper, we propose Intuitionistic Alternating Time Temporal Logic (IATL), an extension of ATL that incorporates intuitionistic logic, providing a specialized representation of imperfect information. We define its syntax, semantics, and key structural properties. Additionally, we propose a PTIME-complete algorithm for IATL model checking, supported by benchmarks demonstrating its efficiency.

Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics), all of them assuming homogeneity in the propositional valuation. Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of a given Kripke structure and intervals are fragments of traces. We introduce a quantitative extension of HS over traces, called Difference HS (DHS), allowing one to express timing constraints on the difference among interval lengths (durations). We show that MC and satisfiability of full DHS are in general undecidable, so, we investigate the decidability border for these problems by considering natural syntactical fragments of DHS. In particular, we identify a maximal decidable fragment DHSsimple of DHS proving in addition that the considered problems for this fragment are at least 2EXPSPACE-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHSsimple, the problems are EXPSPACE-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.

We introduce and investigate a powerful hyper logical framework in the linear-time setting, we call generalized HyperLTL with stuttering and contexts (GHyperLTL_SC for short). GHyperLTL_SC unifies known asynchronous extensions of HyperLTL and the well-known extension KLTL of LTL with knowledge modalities under both the synchronous and asynchronous perfect recall semantics. As a main contribution, we individuate a meaningful fragment of GHyperLTL_SC, we call simple GHyperLTL_SC, with a decidable model-checking problem, which is more expressive than HyperLTL and known fragments of asynchronous extensions of HyperLTL with a decidable model-checking problem. Simple GHyperLTL_SC subsumes KLTL under the synchronous semantics and the one-agent fragment of KLTL under the asynchronous semantics, and to the best of our knowledge, it represents the unique hyper logic with a decidable model-checking problem which can express powerful non-regular trace properties when interpreted on singleton sets of traces. We justify the relevance of simple GHyperLTL_SC by showing that it can express diagnosability properties, interesting classes of information-flow security policies, both in the synchronous and asynchronous settings, and bounded termination (more in general, global promptness in the style of Prompt LTL).

Characterisations theorems serve as important tools in model theory and can be used to assess and compare the expressive power of temporal languages used for the specification and verification of properties in formal methods. While complete connections have been established for the linear-time case between temporal logics, predicate logics, algebraic models, and automata, the situation in the branching-time case remains considerably more fragmented. In this work, we provide an automata-theoretic characterisation of some important branching-time temporal logics, namely CTL* and ECTL* interpreted on arbitrary-branching trees, by identifying two variants of Hesitant Tree Automata that are proved equivalent to those logics. The characterisations also apply to Monadic Path Logic and the bisimulation-invariant fragment of Monadic Chain Logic, again interpreted over trees. These results widen the characterisation landscape of the branching-time case and solve a forty-year-old open question.

A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of chop under the homogeneity assumption. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first consider the logic $\mathsf{BD}_{hom}$ featuring modalities $B$, for \emph{begins}, corresponding to the prefix relation on pairs of intervals, and $D$, for \emph{during}, corresponding to the infix relation. The homogeneous models of $\mathsf{BD}_{hom}$ naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations. Such a fragment has been recently shown to be PSPACE-complete . In this paper, we study the extension $\mathsf{BD}_{hom}$ with the temporal neighborhood modality $A$ (corresponding to the Allen relation \emph{Meets}), and prove that it increases both its expressiveness and complexity. In particular, we show that the resulting logic $\mathsf{BDA}_{hom}$ is EXPSPACE-complete.

We establish the precise complexity of the model-checking problem for the main logics of knowledge and time. While this problem was known to be non-elementary for agents with perfect recall, with a number of exponentials that increases with the alternation of knowledge operators, the precise complexity of the problem when the maximum alternation is fixed has been an open problem for 20 years. We close it by establishing improved upper bounds for CTL * with knowledge and providing matching lower bounds that also apply for epistemic extensions of LTL and CTL . We also study the model-checking problem for these logics on systems satisfying the “no learning” property, introduced by Halpern and Vardi in their taxonomy of logics of knowledge and time, and we settle the complexity in almost all cases.

Monadic Second-Order Logic (MSO) extends First-Order Logic (FO) with variables ranging over sets and quantifications over those variables. We introduce and study Monadic Tree Logic (MTL), a fragment of MSO interpreted on infinite-tree models, where the sets over which the variables range are arbitrary subtrees of the original model. We analyse the expressiveness of MTL compared with variants of MSO and MPL, namely MSO with quantifications over paths. We also discuss the connections with temporal logics, by providing non-trivial fragments of the Graded µ-CALCULUS that can be embedded into MTL and by showing that MTL is enough to encode temporal logics for reasoning about strategies with FO-definable goals.

In this paper, we prove Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality , for the “suffix” relation on pairs of intervals, and modality , for the “sub-interval” relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes () or, symmetrically, the modality for prefixes () to the logic of sub-intervals (featuring only ).

In this article, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures enforcing visibility of the pushdown operations. The proposed logic, called nested BHS , supports branching-time both in the past and in the future and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [ 4 ] and NWTL [ 2 ]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS . The proof exploits a non-trivial automata-theoretic construction.

Hyperproperties are properties of systems that relate different executions traces, with many applications from security to symmetry, consistency models of concurrency, etc. In recent years, different linear-time logics for specifying asynchronous hyperproperties have been investigated. Though model checking of these logics is undecidable, useful decidable fragments have been identified with applications e.g. for asynchronous security analysis. In this paper, we address expressiveness and decidability issues of temporal logics for asynchronous hyperproperties. We compare the expressiveness of these logics together with the extension S1S[E] of S1S with the equal-level predicate by obtaining an almost complete expressiveness picture. We also study the expressive power of these logics when interpreted on singleton sets of traces. We show that for two asynchronous extensions of HyperLTL, checking the existence of a singleton model is already undecidable, and for one of them, namely Context HyperLTL (HyperLTL_C), we establish a characterization of the singleton models in terms of the extension of standard FO[<] over traces with addition. This last result generalizes the well-known equivalence between FO[<] and LTL. Finally, we identify new boundaries on the decidability of model checking HyperLTL_C.

Model checking for Halpern and Shoham's interval temporal logic HS has been recently investigated in a systematic way, and it is known to be decidable under three distinct semantics (state-based, trace-based and tree-based semantics). Here, we focus on the trace-based semantics, where the main semantic entities are the infinite execution paths (traces) of the given Kripke structure, assuming in addition homogeneity in the propositional valuation. We introduce a quantitative extension of HS over traces, called Difference HS (DHS) allowing one to express timing constraints on the difference among interval lengths (durations). The quantitative extension of some modalities leads immediately to undecidability, so, we investigate the decidability border for the model checking and satisfiability problems by considering strict syntactical fragments of DHS. In particular, we identify the maximal decidable fragment DHSS of DHS proving in addition that the considered problems for the fragment are at least 2EXPSPACE-hard. Moreover, by exploiting new results on linear-time hybrid logics, we show that for an equally expressive fragment of DHSS, the problems are EXPSPACE-complete. Finally, we provide a characterization of HS over traces by means of the one-variable fragment of a novel hybrid logic.

The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for the sub-interval relation, under the homogeneity assumption (that constrains a proposition letter to hold over an interval if and only if it holds over all its points). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.

Hyperproperties are a modern specification paradigm that extends trace properties to express properties of sets of traces. Temporal logics for hyperproperties studied in the literature, including HyperLTL, assume a synchronous semantics and enjoy a decidable model checking problem. In this paper, we introduce two asynchronous and orthogonal extensions of HyperLTL, namely Stuttering HyperLTL (HyperLTLS) and Context HyperLTL (HyperLTLC). Both of these extensions are useful, for instance, to formulate asynchronous variants of information-flow security properties. We show that for these logics, model checking is in general undecidable. On the positive side, for each of them, we identify a fragment with a decidable model checking that subsumes HyperLTL and that can express meaningful asynchronous requirements. Moreover, we provide the exact computational complexity of model checking for these two fragments which, for the HyperLTLS fragment, coincides with that of the strictly less expressive logic HyperLTL.

In this paper, we establish Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality ⟨E⟩, for the "suffix" relation on pairs of intervals, and modality ⟨D⟩, for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes (⟨E⟩) or, symmetrically, the modality for prefixes (⟨B⟩) to the logic of sub-intervals (featuring only ⟨D⟩).

In this paper, we investigate the module-checking problem of pushdown multi-agent systems (PMS) against ATL and ATL* specifications. We establish that for ATL, module checking of PMS is 2EXPTIME-complete, which is the same complexity as pushdown module-checking for CTL. On the other hand, we show that ATL* module-checking of PMS turns out to be 4EXPTIME-complete, hence exponentially harder than both CTL* pushdown module-checking and ATL* model-checking of PMS. Our result for ATL* provides a rare example of a natural decision problem that is elementary yet but with a complexity that is higher than triply exponential-time.

A classic result by Stockmeyer [Stockmeyer, 1974] gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of the chop operator under the homogeneity assumption [Halpern et al., 1983]. In this paper, we study the complexity of the satisfiability problem for a suitable weakening of the chop interval temporal logic, that can be equivalently viewed as a fragment of Halpern and Shoham interval logic featuring the operators B, for "begins", corresponding to the prefix relation on pairs of intervals, and D, for "during", corresponding to the infix relation. The homogeneous models of the considered logic naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations.

The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable. In this paper, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, which allow to express meaningful properties. Both semantics are based on the minimality in the time distances of the existentially-quantified time events from the universally-quantified reference event, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small difference in the two semantics, for the strong minimal one, the TP problem is still undecidable, while for the weak minimal one, the TP problem is just PSPACE-complete. Membership in PSPACE is determined by exploiting a strictly more expressive extension (ECA^+) of the well-known robust class of Event-Clock Automata (ECA) that allows to encode the weak minimal TP problem and to reduce it to non-emptiness of Timed Automata (TA). Finally, an extension of ECA^+ (ECA^{++}) is considered, proving that its non-emptiness problem is undecidable. We believe that the two extensions of ECA (ECA^+ and ECA^{++}), introduced for technical reasons, are actually valuable per sé in the field of TA.

The model-checking (MC) problem of Halpern and Shoham Interval Temporal Logic (HS) has been recently investigated in some papers and is known to be decidable. An intriguing open question concerns the exact complexity of the problem for full HS: it is at least EXPSPACE-hard, while the only known upper bound is non-elementary and is obtained by exploiting an abstract representation of Kripke structure paths called descriptors. In this paper we generalize the approach by providing a uniform framework for model-checking full HS and meaningful (almost maximal) fragments, where a specialized type of descriptor is defined for each fragment. We then devise a general MC alternating algorithm parameterized by the type of descriptor which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the time complexity of the algorithm and give, by non-trivial arguments, tight bounds on the length of certificates. For two types of descriptors, we obtain exponential upper and lower bounds which lead to an elementary MC algorithm for the related HS fragments. For the other types of descriptors, we provide non-elementary lower bounds. This last result addresses a question left open in some papers regarding the possibility of fixing an elementary upper bound on the size of the descriptors for full HS.

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham’s interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL*. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL*, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL*).

We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard CTL^* (resp., ATL^*). We establish by formal non-trivial arguments that the "memoryful" linear-past extension (the history leading to the current state is taken into account) can be exponentially more succinct than the standard "local" linear-past extension (the history leading to the current state is forgotten). As a second contribution, we consider the ATL-like fragment, denoted ATL_{lp}, of the known "memoryful" linear-past extension of ATL^{*}. We show that ATL_{lp} is strictly more expressive than ATL, and interestingly, it can be exponentially more succinct than the more expressive logic ATL^{*}. Moreover, we prove that both satisfiability and model-checking for the logic ATL_{lp} are Exptime-complete.

In this paper, we investigate the finite satisfiability and model checking problems for the logic D of the sub-interval relation under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over all its points. First, we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then, we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well.

Cost-parity games are a fundamental tool in system design for the analysis of reactive and distributed systems that recently have received a lot of attention from the formal methods research community. They allow to reason about the time delay on the requests granted by systems, with a bounded consumption of resources, in their executions. In this paper, we contribute to research on Cost-parity games by combining them with hierarchical systems, a successful method for the succinct representation of models. We show that determining the winner of a Hierarchical Cost-parity Game is PSpace-Complete, thus matching the complexity of the proper special case of Hierarchical Parity Games. This shows that reasoning about temporal delay can be addressed at a free cost in terms of complexity.

In the last years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted "point-wise" describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted "interval-wise" express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this paper, we study the expressiveness of Halpern and Shoham's interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL*. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al., that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL*, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL*).

Temporal Equilibrium Logic (TEL) [1] 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 EXPSPACE upper bound in [2]. 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.

Regular Expressions (RE) are an algebraic formalism for expressing regular languages, widely used in string search and as a specification language in verification. In this paper we introduce and investigate Visibly Rational Expressions (VRE), an extension of RE for the well-known class of Visibly Pushdown Languages (VPL). We show that VRE capture the class of VPL. Moreover, we identify an equally expressive fragment of VRE which admits a quadratic time compositional translation into the automata acceptors of VPL. We also prove that, for this fragment, universality, inclusion and language equivalence are EXPTIME-complete. Finally, we provide an extension of VRE for VPL over infinite words.

We address the problem of alternating simulation refinement for concurrent timed games (\TG). We show that checking timed alternating simulation between\TG is \EXPTIME-complete, and provide a logical characterization of thispreorder in terms of a meaningful fragment of a new logic, \TAMTLSTAR.\TAMTLSTAR is an action-based timed extension of standard alternating-timetemporal logic \ATLSTAR, which allows to quantify on strategies where thedesignated player is not responsible for blocking time. While for full \TAMTLSTAR, model-checking \TG is undecidable, we show that for its fragment \TAMTL, corresponding to the timed version of \ATL, in \EXPTIME.

.We investigate the complexity of satisfiability and pushdown model-checking of the extension of the logic CaRet with the binary regular modality 'Chop'. We present automata-theoretic decision procedures based on a direct and compositional construction, which for finite (resp., infinite) words require time of exponential height equal to the nesting depth of chop modality plus one (resp., plus two). Moreover, we provide lower bounds which match the upper bounds for the case of finite words.