Laura Bozzelli

TCS Journal 2025 Journal Article

A quantitative extension of interval temporal logic over infinite words

• Laura Bozzelli
• Adriano Peron

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 DHS s i m p l e 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 DHS s i m p l e, 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.

KR Conference 2025 Conference Paper

An Intuitionistic Version of Alternating-Time Temporal Logic

• Laura Bozzelli
• Andrea Capone
• Davide Catta
• Aniello Murano

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.

EUMAS Conference 2025 Conference Paper

An Intuitionistic Version of Computation Tree Logic

• Andrea Capone
• Laura Bozzelli
• Davide Catta
• Vadim Malvone
• Aniello Murano

TIME Conference 2024 Conference Paper

Full Characterisation of Extended CTL

• Massimo Benerecetti
• Laura Bozzelli
• Fabio Mogavero
• Adriano Peron

The precise identification of the expressive power of logic languages used in formal methods for specifying and verifying run-time properties of critical systems is a fundamental task and characterisation theorems play a crucial role as model-theoretic tools in this regard. While a clear picture of the expressive power of linear-time temporal logics in terms of word automata and predicate logics has long been established, a complete mapping of the corresponding relationships for branching-time temporal logics has proven to be a more elusive task over the past four decades with few scattered results. Only recently, an automata-theoretic characterisation of both CTL* and its full-ω-regular extension ECTL* has been provided in terms of Symmetric Hesitant Tree Automata (HTA), with and without a suitable counter-freeness restriction on their linear behaviours. These two temporal logics also correspond to the bisimulation-invariant semantic fragments of Monadic Path Logic (MPL) and Monadic Chain Logic (MCL), respectively. Additionally, it has been proven that the counting extensions of CTL* and ECTL*, namely CCTL* and CECTL*, enjoy equivalent graded versions of the HTAs for the corresponding non-counting logics. However, while Moller and Rabinovich have proved CCTL* to be equivalent to full MPL, thus filling the gap for the standard branching-time logic, no similar result has been given for CECTL*. This work completes the picture, by proving the expressive equivalence of CECTL* and full MCL, by means of a composition theorem for the latter logic. This also indirectly establishes the equivalence between HTAs and their first-order extensions HFTAs, as originally introduced by Walukiewicz.

I&C Journal 2023 Journal Article

Pspace-completeness of the temporal logic of sub-intervals and suffixes

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron
• Pietro Sala

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 〈 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 〉 ).

TIME Conference 2022 Conference Paper

A Quantitative Extension of Interval Temporal Logic over Infinite Words

• Laura Bozzelli
• Adriano Peron

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 the given Kripke structure. 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 DHS_{simple} 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 DHS_{simple}, 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.

TCS Journal 2022 Journal Article

Complexity issues for timeline-based planning over dense time under future and minimal semantics

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable in the general case. We first prove that the restriction to the future semantics does not suffice to recover decidability. Then, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, and show that they allow one 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 one, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small differences between the two semantics, the TP problem is still undecidable for the strong minimal one, while it is PSPACE-complete for the weak minimal one. 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 us 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. 1

I&C Journal 2022 Journal Article

Context-free timed formalisms: Robust automata and linear temporal logics

• Laura Bozzelli
• Aniello Murano
• Adriano Peron

The paper focuses on automata and linear temporal logics for real-time pushdown reactive systems bridging tractable formalisms specialized for expressing separately dense-time real-time properties and context-free properties though preserving tractability. As for automata, we introduce Event-Clock Nested Automata (ECNA), a formalism that combines Event Clock Automata (ECA) and Visibly Pushdown Automata (VPA). ECNA enjoy the same closure and decidability properties of ECA and VPA expressively extending any previous attempt of combining ECA and VPA. As for temporal logics, we introduce two formalisms for specifying quantitative timing context-free requirements: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). EC_NTL is an extension of both the logic CaRet and Event-Clock Temporal Logic having Exptime-complete satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Systems (VPTS) against EC_NTL. NMTL is a context-free extension of standard Metric Temporal Logic (MTL) which is in general undecidable having, though, a fragment expressively equivalent to EC_NTL with Exptime-complete satisfiability and visibly model-checking of VPTS problems.

GandALF Workshop 2022 Workshop Paper

Parametric Interval Temporal Logic over Infinite Words

• Laura Bozzelli
• Adriano Peron

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. Here, we focus on the trace-based semantics, where the infinite execution paths (traces) of the given (finite) Kripke structure are the main semantic entities. In this setting, each finite infix of a trace is interpreted as an interval, and a proposition holds over an interval if and only if it holds over each component state (homogeneity assumption). In this paper, we introduce a quantitative extension of HS over traces, called parametric HS (PHS). The novel logic allows to express parametric timing constraints on the duration (length) of the intervals. We show that checking the existence of a parameter valuation for which a Kripke structure satisfies a PHS formula (model checking), or a PHS formula admits a trace as a model under the homogeneity assumption (satisfiability) is decidable. Moreover, we identify a fragment of PHS which subsumes parametric LTL and for which model checking and satisfiability are shown to be EXPSPACE-complete.

GandALF Workshop 2021 Workshop Paper

Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron
• Pietro Sala

The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if only if it holds at all its points. The problem for full HS with homogeneity has been shown to be non-elementarily decidable, but its only known lower bound is EXPSPACE (in fact, EXPSPACE-hardness has been shown for the logic of prefixes and suffixes BE, which is a very small fragment of it. The logic of prefixes and infixes BD has been recently shown to be PSPACE-complete. In this paper, we prove that the addition of the Allen relation Meets to BD makes it EXPSPACE-complete.

I&C Journal 2021 Journal Article

Complexity analysis of a unifying algorithm for model checking interval temporal logic

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity for full HS: it is at least EXPSPACE-hard, and the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), is non-elementary. In this paper, we provide a uniform framework to MC for full HS and meaningful fragments of it, with a specific type of descriptor for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the descriptor's type, 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 its complexity and give tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds; for the other ones, we provide non-elementary lower bounds.

TIME Conference 2021 Conference Paper

Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron
• Pietro Sala

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⟩).

TCS Journal 2020 Journal Article

Alternating-time temporal logics with linear past

• Laura Bozzelli
• Aniello Murano
• Loredana Sorrentino

We investigate the succinctness gap between two known equally-expressive and different linear-past extensions of standard 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 l p, of the known ‘memoryful’ linear-past extension of ATL ⁎. We show that ATL l p 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 l p are Exptime -complete.

TCS Journal 2020 Journal Article

Hierarchical cost-parity games

• Laura Bozzelli
• Aniello Murano
• Giuseppe Perelli
• Loredana Sorrentino

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.

I&C Journal 2020 Journal Article

Model checking interval temporal logics with regular expressions

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron

In this paper, we investigate the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS) and its fragments, where labeling of intervals is defined by regular expressions. The MC problem for HS has recently emerged as a viable alternative to the traditional (point-based) temporal logic MC. Most expressiveness and complexity results have been obtained by imposing suitable restrictions on interval labeling, namely, by either defining it in terms of interval endpoints, or by constraining a proposition letter to hold over an interval if and only if it holds over each component state (homogeneity assumption). In both cases, the expressiveness of HS gets noticeably limited, in particular when fragments of HS are considered. A possible way to increase the expressiveness of interval temporal logic MC was proposed by Lomuscio and Michaliszyn, who suggested to use regular expressions to define interval labeling, i. e. , the properties that hold true over intervals/computation stretches, based on their component points/system states. In this paper, we provide a systematic account of decidability and complexity issues for model checking HS and its fragments extended with regular expressions. We first prove that MC for (full) HS extended with regular expressions is decidable by an automaton-theoretic argument. Though the exact complexity of full HS MC remains an open issue, the complexity of all relevant proper fragments of HS is here determined. In particular, we provide an asymptotically optimal bound to the complexity of the two syntactically maximal fragments A A ‾ B B ‾ E ‾ and A A ‾ E B ‾ E ‾, by showing that their MC problem is AEX P pol -complete ( AEX P pol is the complexity class of problems decided by exponential-time bounded alternating Turing Machines making a polynomially bounded number of alternations). Moreover, we show that a better result holds for A A ‾ B B ‾, A A ‾ E E ‾ and all their sub-fragments, whose MC problem turns out to be PSPACE-complete.

KR Conference 2020 Conference Paper

Module Checking of Pushdown Multi-agent Systems

• Laura Bozzelli
• Aniello Murano
• Adriano Peron

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.

MFCS Conference 2020 Conference Paper

On a Temporal Logic of Prefixes and Infixes

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron
• Pietro Sala

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.

TCS Journal 2020 Journal Article

Timeline-based planning over dense temporal domains

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron
• Gerhard Woeginger

Planning is one of the most studied problems in computer science. In this paper, we focus on the timeline-based approach, where the domain is modeled by a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (transition functions and synchronization rules). Whereas the time domain is usually assumed to be discrete, here we address decidability and complexity issues for timeline-based planning (TP) over dense time. We first prove that dense TP is undecidable in the general case; then, we show that decidability can be recovered by restricting to synchronization rules with a suitable future semantics. More “tractable” settings can be obtained by additionally constraining the form of intervals used in rules: EXPSPACE-completeness is obtained by avoiding singular intervals, and PSPACE-completeness by admitting only intervals of the forms [ 0, a ] and [ b, + ∞ [. Finally, NP-completeness can be proved for dense TP with purely existential rules only.

TIME Conference 2019 Conference Paper

Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

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.

IJCAI Conference 2019 Conference Paper

The Complexity of Model Checking Knowledge and Time

• Laura Bozzelli
• Bastien Maubert
• Aniello Murano

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 twenty 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.

TCS Journal 2019 Journal Article

Which fragments of the interval temporal logic HS are tractable in model checking?

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron
• Pietro Sala

Since the 80s, model checking (MC) has been applied to the automatic verification of hardware/software systems. Point-based temporal logics, such as LTL, CTL, CTL ⁎, and the like, are commonly used in MC as the specification language; however, there are some inherently interval-based properties of computations, e. g. , temporal aggregations and durations, that cannot be properly dealt with by these logics, as they model a state-by-state evolution of systems. Recently, an MC framework for the verification of interval-based properties of computations, based on Halpern and Shoham's interval temporal logic ( HS, for short) and its fragments, has been proposed and systematically investigated. In this paper, we focus on the boundaries that separate tractable and intractable HS fragments in MC. We first prove that MC for the logic BE of Allen's relations started-by and finished-by is provably intractable, being Expspace-hard. Such a lower bound immediately propagates to full HS. Then, in contrast, we show that other noteworthy HS fragments, i. e. , the logic A A ‾ B B ‾ (resp. , A A ‾ E E ‾ ) of Allen's relations meets, met-by, starts (resp. , finishes), and started-by (resp. , finished-by), are well-behaved, and turn out to have the same complexity as LTL (Pspace-complete). Halfway are the fragments A A ‾ B B ‾ E ‾ and A A ‾ E B ‾ E ‾, whose Expspace membership and Pspace hardness are already known. Here, we give an original proof of Expspace membership, that substantially simplifies the complexity of the constructions previously used for such a result. Contraction techniques—suitably tailored to each HS fragment—are at the heart of our results, enabling us to prove a pair of remarkable small-model properties.

GandALF Workshop 2018 Workshop Paper

Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron

In this paper, we address complexity issues for timeline-based planning over dense temporal domains. The planning problem is modeled by means of a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (synchronization rules). While the temporal domain is usually assumed to be discrete, here we consider the dense case. Dense timeline-based planning has been recently shown to be undecidable in the general case; decidability (NP-completeness) can be recovered by restricting to purely existential synchronization rules (trigger-less rules). In this paper, we investigate the unexplored area of intermediate cases in between these two extremes. We first show that decidability and non-primitive recursive-hardness can be proved by admitting synchronization rules with a trigger, but forcing them to suitably check constraints only in the future with respect to the trigger (future simple rules). More "tractable" results can be obtained by additionally constraining the form of intervals in future simple rules: EXPSPACE-completeness is guaranteed by avoiding singular intervals, PSPACE-completeness by admitting only intervals of the forms [0, a] and [b, +∞[.

KR Conference 2018 Short Paper

Decidability and Complexity of Timeline-based Planning over Dense Temporal Domains

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron

In timeline-based planning, the planning domain is modeled as a set of independent, but interacting, components each one represented by a number of state variables, whose behavior over time (timelines) is governed by temporal constraints (synchronization rules). The temporal domain is typically assumed to be discrete. In this paper, we address decidability and complexity issues for timeline-based planning over dense temporal domains without resorting to any form of discretization. We first prove that the general problem is undecidable, and then we show that decidability can be recovered by constraining the logical structure of synchronization rules.

I&C Journal 2018 Journal Article

Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron
• Pietro Sala

Some temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them. We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in P NP. Additionally, we provide some complexity lower bounds to the problem.

TIME Conference 2018 Conference Paper

Results on Alternating-Time Temporal Logics with Linear Past

• Laura Bozzelli
• Aniello Murano
• Loredana Sorrentino

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.

GandALF Workshop 2018 Workshop Paper

Timed Context-Free Temporal Logics

• Laura Bozzelli
• Aniello Murano
• Adriano Peron

The paper is focused on temporal logics for the description of the behaviour of real-time pushdown reactive systems. The paper is motivated to bridge tractable logics specialized for expressing separately dense-time real-time properties and context-free properties by ensuring decidability and tractability in the combined setting. To this end we introduce two real-time linear temporal logics for specifying quantitative timing context-free requirements in a pointwise semantics setting: Event-Clock Nested Temporal Logic (EC_NTL) and Nested Metric Temporal Logic (NMTL). The logic EC_NTL is an extension of both the logic CaRet (a context-free extension of standard LTL) and Event-Clock Temporal Logic (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of EC_NTL and visibly model-checking of Visibly Pushdown Timed Automata (VPTA) against EC_NTL are decidable and EXPTIME-complete. The other proposed logic NMTL is a context-free extension of standard Metric Temporal Logic (MTL). It is well known that satisfiability of future MTL is undecidable when interpreted over infinite timed words but decidable over finite timed words. On the other hand, we show that by augmenting future MTL with future context-free temporal operators, the satisfiability problem turns out to be undecidable also for finite timed words. On the positive side, we devise a meaningful and decidable fragment of the logic NMTL which is expressively equivalent to EC_NTL and for which satisfiability and visibly model-checking of VPTA are EXPTIME-complete.

TIME Conference 2017 Conference Paper

Hierarchical Cost-Parity Games

• Laura Bozzelli
• Aniello Murano
• Giuseppe Perelli
• Loredana Sorrentino

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.

GandALF Workshop 2017 Workshop Paper

On the Complexity of ATL and ATL* Module Checking

• Laura Bozzelli
• Aniello Murano

Module checking has been introduced in late 1990s to verify open systems, i. e. , systems whose behavior depends on the continuous interaction with the environment. Classically, module checking has been investigated with respect to specifications given as CTL and CTL* formulas. Recently, it has been shown that CTL (resp. , CTL*) module checking offers a distinctly different perspective from the better-known problem of ATL (resp. , ATL*) model checking. In particular, ATL (resp. , ATL*) module checking strictly enhances the expressiveness of both CTL (resp. , CTL*) module checking and ATL (resp. ATL*) model checking. In this paper, we provide asymptotically optimal bounds on the computational cost of module checking against ATL and ATL*, whose upper bounds are based on an automata-theoretic approach. We show that module-checking for ATL is EXPTIME-complete, which is the same complexity of module checking against CTL. On the other hand, ATL* module checking turns out to be 3EXPTIME-complete, hence exponentially harder than CTL* module checking.

GandALF Workshop 2017 Workshop Paper

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

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron

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.

TCS Journal 2016 Journal Article

Foundations of Boolean stream runtime verification

• Laura Bozzelli
• César Sánchez

Stream runtime verification (SRV), pioneered by the tool LOLA, is a declarative formalism to specify synchronous monitors. In SRV, monitors are described by specifying dependencies between output streams of values and input streams of values. The declarative nature of SRV enables a separation between the evaluation algorithms, and the monitor storage and its individual updates. This separation allows SRV to be lifted from conventional failure monitors into richer domains to collect statistics of traces. Moreover, SRV allows to easily identify specifications that can be efficiently monitored online, and to generate efficient schedules for offline monitors. In spite of these attractive features, many important theoretical problems about SRV are still open. In this paper, we address complexity, expressiveness, succinctness, and closure issues for the subclass of Boolean SRV (BSRV) specifications. Additionally, we show that for this subclass, offline monitoring can be performed with only two passes (one forward and one backward) over the input trace in spite of the alternation of past and future references in the BSRV specification.

GandALF Workshop 2016 Workshop Paper

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

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron
• Pietro Sala

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).

JELIA Conference 2016 Conference Paper

On the Expressiveness of Temporal Equilibrium Logic

• Laura Bozzelli
• David Pearce 0001

Abstract We investigate expressiveness issues of Temporal Equilibrium Logic ( TEL ), a promising nonmonotonic logical framework for temporal reasoning. TEL shares the syntax of standard linear temporal logic LTL, but its semantics is an orthogonal combination of the LTL semantics with the nonmonotonic semantics of Equilibrium Logic. We establish that TEL is more expressive than LTL, and captures a strict subclass of \(\omega \) -regular languages. We illustrate the expressive power of \(\textsf {TEL} \) by showing that \(\textsf {LTL} \) -conformant planning, which is not expressible in \(\textsf {LTL} \), can be instead expressed in \(\textsf {TEL} \). Additionally, we provide a systematic study of the expressiveness comparison between the LTL semantics and the TEL semantics for various natural syntactical fragments.

TCS Journal 2015 Journal Article

The complexity of one-agent refinement modal logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

We investigate the complexity of satisfiability for one-agent refinement modal logic (RML), a known extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures. It is known that RML has the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper, we show that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem. More precisely, we establish that RML-satisfiability is complete for the complexity class AEXP pol, i. e. , the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations (note that NEXPTIME ⊆ AEXP pol ⊆ EXPSPACE ). 1 1 This work is the revised and expanded version of [1].

I&C Journal 2015 Journal Article

Uniform strategies, rational relations and jumping automata

• Laura Bozzelli
• Bastien Maubert
• Sophie Pinchinat

A general concept of uniform strategies has recently been proposed as a relevant notion in game theory for computer science, which subsumes various notions from the literature. It relies on properties involving sets of plays in two-player turn-based arenas equipped with arbitrary binary relations between plays; these properties are expressed in a language based on CTL ⁎ with a quantifier over related plays. There are two semantics for our quantifier, a strict one and a full one, that we study separately. Regarding the strict semantics, the existence of a uniform strategy is undecidable for rational binary relations, but introducing jumping tree automata and restricting attention to recognizable relations allows us to establish a 2-Exptime-complete complexity – and still capture a class of two-player imperfect-information games with epistemic temporal objectives. Regarding the full semantics, relying on information set automata we establish that the existence of a uniform strategy is decidable for rational relations and we provide a nonelementary synthesis procedure. We also exhibit an essentially optimal subclass of rational relations for which the problem becomes 2-Exptime-complete. Considering rich classes of relations makes the theory of uniform strategies powerful: it directly entails various results in logics of knowledge and time, some of them already known, and others new.

I&C Journal 2014 Journal Article

Refinement modal logic

• Laura Bozzelli
• Hans van Ditmarsch
• Tim French
• James Hales
• Sophie Pinchinat

In this paper we present 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 ∀ in addition to the standard box modalities for each agent. The operator ∀ 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 ∀ 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 μ-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.

TCS Journal 2014 Journal Article

Verification of gap-order constraint abstractions of counter systems

• Laura Bozzelli
• Sophie Pinchinat

We investigate verification problems for gap-order constraint systems ( GCS ), an (infinitely-branching) abstract model of counter machines, in which constraints (over Z ) between the variables of the source state and the target state of a transition are gap-order constraints ( GC ) [32]. GCS extend monotonicity constraint systems [7], integral relation automata [16], and constraint automata in [19]. First, we address termination and fairness analysis of GCS. Since GCS are infinitely-branching, termination does not imply strong termination, i. e. the existence of an upper bound on the lengths of the runs from a given state. We show that the termination problem, the strong termination problem, and the fairness problem for GCS (the latter consisting in checking the existence of infinite runs in GCS satisfying acceptance conditions à la Büchi) are decidable and Pspace-complete. Moreover, for each control location of the given GCS, one can build a GC representation of the set of counter variable valuations from which termination (resp. , strong termination, resp. , fairness) does not hold (resp. , does not hold, resp. , does hold). Next, we consider a constrained branching-time logic, GCCTL ⁎, obtained by enriching CTL ⁎ with GC, thus enabling expressive properties and subsuming the setting of [16]. We establish that, while model-checking GCS against the universal fragment of GCCTL ⁎ is undecidable, model-checking against the existential fragment, and satisfiability of both the universal and existential fragments are instead decidable and Pspace-complete (note that the two fragments are not dual since GC are not closed under negation). Moreover, our results imply Pspace-completeness of known verification problems that were shown to be decidable in [16] with no elementary upper bounds.

IJCAI Conference 2013 Conference Paper

The Complexity of One-Agent Refinement Modal Logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

We investigate the complexity of satisfiability for one-agent refinement modal logic (RML), an extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures. RML is known to have the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper we show that RML-satisfiability is ‘only’ singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem.

JELIA Conference 2012 Conference Paper

The Complexity of One-Agent Refinement Modal Logic

• Laura Bozzelli
• Hans van Ditmarsch
• Sophie Pinchinat

Abstract We investigate the complexity of satisfiability for one-agent Refinement Modal Logic ( \(\text{\sffamily RML}\) ), a known extension of basic modal logic ( \(\text{\sffamily ML}\) ) obtained by adding refinement quantifiers on structures. It is known that \(\text{\sffamily RML}\) has the same expressiveness as \(\text{\sffamily ML}\), but the translation of \(\text{\sffamily RML}\) into \(\text{\sffamily ML}\) is of non-elementary complexity, and \(\text{\sffamily RML}\) is at least doubly exponentially more succinct than \(\text{\sffamily ML}\). In this paper, we show that \(\text{\sffamily RML}\) -satisfiability is ‘only’ singly exponentially harder than \(\text{\sffamily ML}\) -satisfiability, the latter being a well-known PSPACE -complete problem. More precisely, we establish that \(\text{\sffamily RML}\) -satisfiability is complete for the complexity class AEXP \(_{\text{\sffamily pol}}\), i. e. , the class of problems solvable by alternating Turing machines running in single exponential time but only with a polynomial number of alternations (note that NEXPTIME ⊆ AEXP \(_{\text{\sffamily pol}}\) ⊆ EXPSPACE ).

TCS Journal 2011 Journal Article

Hardness of preorder checking for basic formalisms

• Laura Bozzelli
• Axel Legay
• Sophie Pinchinat

We investigate the complexity of preorder checking when the specification is a flat finite-state system whereas the implementation is either a non-flat finite-state system or a standard timed automaton. In both cases, we show that simulation checking is Exptime-hard, and for the case of a non-flat implementation, the result holds even if there is no synchronization between the parallel components and their alphabets of actions are pairwise disjoint. Moreover, we show that the considered problems become Pspace-complete when the specification is assumed to be deterministic. Additionally, we establish that comparing a synchronous non-flat system with no hiding and a flat system is Pspace-hard for any relation between trace containment and bisimulation equivalence, even if the flat system is assumed to be fixed.

GandALF Workshop 2011 Workshop Paper

New results on pushdown module checking with imperfect information

• Laura Bozzelli

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).

GandALF Workshop 2011 Workshop Paper

Opacity Issues in Games with Imperfect Information

• Bastien Maubert
• Sophie Pinchinat
• Laura Bozzelli

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.

TCS Journal 2010 Journal Article

Complexity and succinctness issues for linear-time hybrid logics

• Laura Bozzelli
• Ruggero Lanotte

Full linear-time hybrid logic (HL) is a non-elementary and equally expressive extension of standard LTL + past obtained by adding the well-known binder operators ↓ and ∃. We investigate complexity and succinctness issues for HL in terms of the number of variables and nesting depth of binder modalities. First, we present direct automata-theoretic decision procedures for satisfiability and model-checking of HL, which require space of exponential height equal to the nesting depth of the binder modalities. The proposed algorithms are proved to be asymptotically optimal by providing matching lower bounds. Second, we show that, for the one-variable fragment of HL, the considered problems are elementary and, precisely, Expspace-complete. Finally, we show that, for all 0 ≤ h < k, there is a succinctness gap between the fragments HL k and HL h with binder nesting depth at most k and h, respectively, of exponential height equal to k − h.

JELIA Conference 2008 Conference Paper

Complexity and Succinctness Issues for Linear-Time Hybrid Logics

• Laura Bozzelli
• Ruggero Lanotte

Abstract Full linear-time hybrid logic ( HL ) is a non-elementary and equally expressive extension of standard LTL + past obtained by adding the well-known binder operators ↓ and ∃. We investigate complexity and succinctness issues for HL in terms of the number of variables and nesting depth of binder modalities. First, we present direct automata-theoretic decision procedures for satisfiability and model-checking of HL, which require space of exponential height equal to the nesting depth of binder modalities. The proposed algorithms are proved to be asymptotically optimal by providing matching lower bounds. Second, we show that for the one-variable fragment of HL, the considered problems are elementary and, precisely, Expspace -complete. Finally, we show that for all 0 ≤ h < k, there is a succinctness gap between the fragments HL k and HL h with binder nesting depth at most k and h, respectively, of exponential height equal to k − h.

TIME Conference 2008 Conference Paper

The Complexity of CaRet + Chop

• Laura Bozzelli

. 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.

TCS Journal 2008 Journal Article

Verification of well-formed communicating recursive state machines

• Laura Bozzelli
• Salvatore La Torre
• Adriano Peron

In this paper we introduce a new (non-Turing equivalent) formal model of recursive concurrent programs called well-formed communicating recursive state machines (CRSM). CRSM extend recursive state machines (RSM) by allowing a restricted form of concurrency: a state of a module can be refined into a finite collection of modules (working in parallel) in a potentially recursive manner. Communication is only possible between the activations of modules invoked on the same fork. We study the model-checking problem of CRSM with respect to specifications expressed in a temporal logic that extends CaRet with a parallel operator (ConCaRet). We propose a decision algorithm that runs in time exponential in both the size of the formula and the maximum number of modules that can be invoked simultaneously. This matches the known lower bound for deciding CaRet model checking of RSM, and therefore, we prove that model checking CRSM with respect to ConCaRet specifications is Exptime-complete.

TCS Journal 2007 Journal Article

Complexity results on branching-time pushdown model checking

• Laura Bozzelli

The model checking problem of pushdown systems (PMC problem, for short) against standard branching temporal logics has been intensively studied in the literature. In particular, for the modal μ -calculus, the most powerful branching temporal logic used for verification, the problem is known to be Exptime-complete (even for a fixed formula). The problem remains Exptime-complete also for the logic CTL, which corresponds to a fragment of the alternation-free modal μ -calculus. For the logic CTL ∗, the problem is known to be in 2Exptime. In this paper, we show that the complexity of the PMC problem for CTL ∗ is in fact 2Exptime-complete. Moreover, we give a new optimal algorithm to solve this problem based on automata theoretic techniques. Finally, we prove that the program complexity of the PMC problem against CTL (i. e. , the complexity of the problem in terms of the size of the system) is Exptime-complete.

LPAR Conference 2006 Conference Paper

Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints

• Laura Bozzelli
• Régis Gascon

Abstract Recently, LTL extended with atomic formulas built over a constraint language interpreting variables in ℤ has been shown to have a decidable satisfiability and model-checking problem. This language allows to compare the variables at different states of the model and include periodicity constraints, comparison constraints, and a restricted form of quantification. On the other hand, the CTL counterpart of this logic (and hence also its CTL* counterpart which subsumes both LTL and CTL ) has an undecidable model-checking problem. In this paper, we substantially extend the decidability border, by considering a meaningful fragment of CTL* extended with such constraints (which subsumes both the universal and existential fragments, as well as the EF -like fragment) and show that satisfiability and model-checking over relational automata that are abstraction of counter machines are decidable. The correctness and the termination of our algorithm rely on a suitable well quasi-ordering defined over the set of variable valuations.

TCS Journal 2006 Journal Article

Model checking for process rewrite systems and a class of action-based regular properties

• Laura Bozzelli

We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against 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 PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL.

LPAR Conference 2005 Conference Paper

Pushdown Module Checking

• Laura Bozzelli
• Aniello Murano
• Adriano Peron

Abstract Model checking is a useful method to verify automatically the correctness of a system with respect to a desired behavior, by checking whether a mathematical model of the system satisfies a formal specification of this behavior. Many systems of interest are open, in the sense that their behavior depends on the interaction with their environment. The model checking problem for finite–state open systems (called module checking ) has been intensively studied in the literature. In this paper, we focus on open pushdown systems and we study the related model–checking problem ( pushdown module checking, for short) with respect to properties expressed by CTL and CTL * formulas. We show that pushdown module checking against CTL (resp. , CTL *) is 2 Exptime -complete (resp. , 3 Exptime -complete). Moreover, we prove that for a fixed CTL * formula, the problem is Exptime -complete.