Author name cluster

Adriano Peron

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

39 papers

2 author rows

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.

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

I&C Journal 2023 Journal Article

Taming Strategy Logic: Non-Recurrent Fragments

Massimo Benerecetti
Fabio Mogavero
Adriano Peron

Strategy Logic ( Image 1 for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends Image 2 with first-order quantifiers over the agent strategies and encompasses other formalisms, such as Image 3 and Image 4. The model-checking problem for Image 1 and several of its fragments has been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal Image 1, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these two logics, and for the corresponding fragments of Image 3 and Image 4, is in Image 5 and Image 6, respectively.

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.

PDF Details DOI

TIME Conference 2022 Conference Paper

Taming Strategy Logic: Non-Recurrent Fragments

Massimo Benerecetti
Fabio Mogavero
Adriano Peron

Strategy Logic (SL for short) is one of the prominent languages for reasoning about the strategic abilities of agents in a multi-agent setting. This logic extends LTL with first-order quantifiers over the agent strategies and encompasses other formalisms, such as ATL* and CTL*. The model-checking problem for SL and several of its fragments have been extensively studied. On the other hand, the picture is much less clear on the satisfiability front, where the problem is undecidable for the full logic. In this work, we study two fragments of One-Goal SL, where the nesting of sentences within temporal operators is constrained. We show that the satisfiability problem for these logics, and for the corresponding fragments of ATL* and CTL*, is ExpSpace and PSpace-Complete, respectively.

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.

PDF Details DOI

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

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.

PDF Details DOI

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.

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, +∞[.

PDF Details DOI

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 Halpern and Shoham's interval temporal logic based on track representatives

Alberto Molinari
Angelo Montanari
Adriano Peron

Model checking allows one to automatically verify a specification of the expected properties of a system against a formal model of its behavior (generally, a Kripke structure). Point-based temporal logics, such as LTL, CTL, and CTL⁎, that describe how the system evolves state-by-state, are commonly used as specification languages. They proved themselves quite successful in a variety of application domains. However, properties constraining the temporal ordering of temporally extended events as well as properties involving temporal aggregations, which are inherently interval-based, can not be properly dealt with by them. Interval temporal logics (ITLs), that take intervals as their primitive temporal entities, turn out to be well-suited for the specification and verification of interval properties of computations (we interpret all the tracks of a Kripke structure as computation intervals). In this paper, we study the model checking problem for some fragments of Halpern and Shoham's modal logic of time intervals (HS). HS features one modality for each possible ordering relation between pairs of intervals (the so-called Allen's relations). First, we describe an EXPSPACE model checking algorithm for the HS fragment of Allen's relations meets, met-by, starts, started-by, and finishes, which exploits the possibility of finding, for each track (of unbounded length), an equivalent bounded-length track representative. While checking a property, it only needs to consider tracks whose length does not exceed the given bound. Then, we prove the model checking problem for such a fragment to be PSPACE-hard. Finally, we identify other well-behaved HS fragments which are expressive enough to capture meaningful interval properties of systems, such as mutual exclusion, state reachability, and non-starvation, and whose computational complexity is less than or equal to that of LTL.

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.

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.

PDF Details DOI

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.

PDF Details DOI

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

PDF Details DOI

KR Conference 2016 Conference Paper

Model checking well-behaved fragments of HS: the (almost) final picture

Alberto Molinari
Angelo Montanari
Adriano Peron
Pietro Sala

Model checking is one of the most powerful and widespread tools for system veriﬁcation with applications in many areas of computer science and artiﬁcial intelligence. The large majority of model checkers deal with properties expressed in point-based temporal logics, such as LTL and CTL. However, there exist relevant properties of systems which are inherently interval-based. Model checking algorithms for interval temporal logics (ITLs) have recently been proposed to check interval properties of computations. As the model checking problem for full Halpern and Shoham’s ITL (HS for short) turns out to be decidable, but computationally heavy, research has focused on its well-behaved fragments. In this paper, we provide an almost ﬁnal picture of the computational complexity of model checking for HS fragments with modalities for (a subset of) Allen’s relations meets, met by, starts, and ends.

TCS Journal 2016 Journal Article

Ordered multi-stack visibly pushdown automata

Dario Carotenuto
Aniello Murano
Adriano Peron

Visibly Pushdown Automata (VPA) are a special case of pushdown machines where the stack operations are driven by the input. In this paper, we consider VPA with multiple stacks, namely n-VPA, with n > 1. These automata introduce a useful model to effectively describe concurrent pushdown systems using a simple communication mechanism between stacks. We show that n-VPA are strictly more expressive than VPA. Indeed, n-VPA accept some context-sensitive languages that are not context-free and some context-free languages that are not accepted by any VPA. Nevertheless, we show that the class of languages accepted by n-VPA is closed under union and intersection. On the contrary, this class turns out to be neither closed under complementation nor determinizable. Moreover, we show that the emptiness problem for n-VPA is undecidable. By adding an ordering constraint on stacks (n-OVPA), decidability of emptiness can be recovered, as well as the closure under complementation. Using these properties along with the automata-theoretic approach, one can prove that the model checking problem over n-OVPA models against n-OVPA specifications is decidable.

TCS Journal 2016 Journal Article

Timed recursive state machines: Expressiveness and complexity

Massimo Benerecetti
Adriano Peron

The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs), which consists of an indexed collection of Timed Automata, called components. Each component can invoke other components in a potentially recursive manner. Besides being able to model procedure calls and recursion, TRSMs are equipped with the ability to suspend the evolution of time within a component when another component is invoked and to recover it when control is given back at return time. This mechanism is realized by storing clock valuations into an implicit stack at invocation time and restoring them upon return. Indeed, TRSMs can be related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. The expressiveness and computational properties of the resulting model are analyzed, showing that it can be used to recognize timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case. However, the problem becomes decidable for two meaningful subclasses, called I-TRSM and L-TRSM, obtained by suitably constraining the set of clocks to reset at invocation time and to restore at return time. The considered subclasses are compared with the corresponding EPTAs subclasses through bisimulation of their timed LTSs. The complexity of the reachability problem for L-TRSM and I-TRSM is proved to be EXPTIME-complete and PSPACE-complete, respectively. Moreover, we prove that such classes strictly enhance the expressive power of Timed Automata and of Pushdown Timed Automata, forming a proper hierarchy.

CSL Conference 2015 Conference Paper

A Model Checking Procedure for Interval Temporal Logics based on Track Representatives

Alberto Molinari
Angelo Montanari
Adriano Peron

Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones.

TIME Conference 2015 Conference Paper

Complexity of ITL Model Checking: Some Well-Behaved Fragments of the Interval Logic HS

Alberto Molinari
Angelo Montanari
Adriano Peron

Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we show that more efficient model checking procedures can be developed for some expressive enough fragments of HS.

TIME Conference 2014 Conference Paper

Checking Interval Properties of Computations

Angelo Montanari
Aniello Murano
Giuseppe Perelli
Adriano Peron

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e. g. A Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments AAbarBBbar and AAbarEEbar.

TIME Conference 2010 Conference Paper

Analysis of Timed Recursive State Machines

Massimo Benerecetti
Stefano Minopoli
Adriano Peron

The paper proposes a temporal extension of Recursive State Machines (RSMs), called Timed RSMs (TRSMs). A TRSM is an indexed collection of Timed Automata allowed to invoke other Timed Automata (procedural calls). The classes of TRSMs are related to an extension of Pushdown Timed Automata, called EPTAs, where an additional stack, coupled with the standard control stack, is used to store temporal valuations of clocks. A number of subclasses of TRSMs and EPTAs are considered and compared through bisimulation of their timed LTSs. It is shown that EPTAs and TRSMs can be used to recognize classes of timed languages exhibiting context-free properties not only in the untimed “control” part, but also in the associated temporal dimension. The reachability problem for both TRSMs and EPTAs is investigated, showing that the problem is undecidable in the general case, but decidable for meaningful subclasses. The complexity is stated for a TRSMs subclass.

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.

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.

MFCS Conference 2004 Conference Paper

Structural Model Checking for Communicating Hierarchical Machines

Ruggero Lanotte
Andrea Maggiolo-Schettini
Adriano Peron

Abstract In this paper we consider the problem of model checking for well structured Communicating Hierarchical Machines (CHMs), i. e. Finite State Machines with additional features of hierarchy and concurrency. For model checking we follow the automaton theoretic approach, defining an algorithm which solves the problem of model checking without flattening the structure of CHMs.

TCS Journal 2003 Journal Article

A comparison of Statecharts step semantics

Andrea Maggiolo-Schettini
Adriano Peron
Simone Tini

The paper studies some variants of Statecharts step semantics in the framework of structural operational semantics. The chosen framework allows to study precongruence and congruence properties of behavioral preorders and equivalences and to compare, with respect to these properties, the different step semantics considered.

TIME Conference 2003 Conference Paper

Definability and decidability of binary predicates for time granularity

Massimo Franceschet
Angelo Montanari
Adriano Peron
Guido Sciavicco

In this paper, we study the definability and decidability of binary predicates for time granularity with respect to monadic theories over finitely and infinitely layered structures. We focus our attention on the equi-level (resp. equi-column) predicate constraining two time points to belong to the same layer (resp. column) and on the horizontal (resp. vertical) successor predicate relating a time point to its successor within a given layer (resp. column). We give a number of positive and negative results by reduction to/from a wide spectrum of decidable/undecidable problems.

TIME Conference 2002 Conference Paper

A Logical Approach to Represent and Reason about Calendars

Carlo Combi
Massimo Franceschet
Adriano Peron

We propose a logical approach to represent and reason about different time granularities. We identify a time granularity as a discrete infinite sequence of time points properly labelled with proposition symbols marking the starting and ending points of the corresponding granules, and we intensively model sets of granularities with linear time logic formulas. Some real-world granularities are provided to motivate and exemplify our approach. The proposed framework permits to algorithmically solve the consistency, the equivalence, and the classification problems in a uniform way, by reducing them to the validity problem for the considered linear time logic.

TCS Journal 2000 Journal Article

Systolic tree ω-languages: the operational and the logical view

Angelo Monti
Adriano Peron

The class of ω-languages recognized by systolic (binary) tree automata is introduced. This class extends the class of Büchi ω-languages though maintaining the closure under union, intersection and complement and the decidability of emptiness. The class of systolic tree ω-languages is characterized in terms of a (suitable) concatenation of (finitary) systolic tree languages. A generalization of Buc̈hi Theorem is provided which establishes a correspondence between systolic tree ω-languages and a suitable extension of the sequential calculus S1S.