Recent zbMATH articles by "Bozzelli, Laura"https://zbmath.org/atom/ai/bozzelli.laura2024-03-13T18:33:02.981707ZWerkzeugTimed context-free temporal logicshttps://zbmath.org/1528.682122024-03-13T18:33:02.981707Z"Bozzelli, Laura"https://zbmath.org/authors/?q=ai:bozzelli.laura"Murano, Aniello"https://zbmath.org/authors/?q=ai:murano.aniello"Peron, Adriano"https://zbmath.org/authors/?q=ai:peron.adrianoSummary: 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: \textit{Event-Clock Nested Temporal Logic} (\textsf{EC\_NTL}) and \textit{Nested Metric Temporal Logic} (\textsf{NMTL}). The logic \textsf{EC\_NTL} is an extension of both the logic CaRet (a context-free extension of standard \textsf{LTL}) and \textit{Event-Clock Temporal Logic} (a tractable real-time logical framework related to the class of Event-Clock automata). We prove that satisfiability of \textsf{EC\_NTL} and visibly model-checking of Visibly Pushdown Timed Automata (\textsf{VPTA}) against \textsf{EC\_NTL} are decidable and \textsc{Exptime}-complete. The other proposed logic \textsf{NMTL} is a context-free extension of standard Metric Temporal Logic (\textsf{MTL}). It is well known that satisfiability of future \textsf{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 \textsf{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 \textsf{NMTL} which is expressively equivalent to \textsf{EC\_NTL} and for which satisfiability and visibly model-checking of \textsf{VPTA} are \textsc{Exptime}-complete.
For the entire collection see [Zbl 1436.68032].Context-free timed formalisms: robust automata and linear temporal logicshttps://zbmath.org/1528.682132024-03-13T18:33:02.981707Z"Bozzelli, Laura"https://zbmath.org/authors/?q=ai:bozzelli.laura"Murano, Aniello"https://zbmath.org/authors/?q=ai:murano.aniello"Peron, Adriano"https://zbmath.org/authors/?q=ai:peron.adrianoSummary: 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: \textit{Event-Clock Nested Temporal Logic} (EC\_NTL) and \textit{Nested Metric Temporal Logic} (NMTL). (EC\_NTL) is an extension of both the logic CaRet and \textit{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.Complexity of timeline-based planning over dense temporal domains: exploring the middle groundhttps://zbmath.org/1528.683582024-03-13T18:33:02.981707Z"Bozzelli, Laura"https://zbmath.org/authors/?q=ai:bozzelli.laura"Molinari, Alberto"https://zbmath.org/authors/?q=ai:molinari.alberto"Montanari, Angelo"https://zbmath.org/authors/?q=ai:montanari.angelo"Peron, Adriano"https://zbmath.org/authors/?q=ai:peron.adrianoSummary: 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 (\textbf{NP}-completeness) can be recovered by restricting to purely existential synchronization rules (\textit{trigger-less rules}). In this paper, we investigate the unexplored area of intermediate cases in between these two extremes. We first show that \textbf{decidability} and \textbf{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 (\textit{future simple rules}). More ``tractable'' results can be obtained by additionally constraining the form of intervals in future simple rules: \textbf{EXPSPACE}-completeness is guaranteed by avoiding singular intervals, \textbf{PSPACE}-completeness by admitting only intervals of the forms \([0, a]\) and \([b, +\infty[\).
For the entire collection see [Zbl 1436.68032].Taming the complexity of timeline-based planning over dense temporal domainshttps://zbmath.org/1528.683592024-03-13T18:33:02.981707Z"Bozzelli, Laura"https://zbmath.org/authors/?q=ai:bozzelli.laura"Montanari, Angelo"https://zbmath.org/authors/?q=ai:montanari.angelo"Peron, Adriano"https://zbmath.org/authors/?q=ai:peron.adrianoSummary: The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable. In this paper, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, which allow to express meaningful properties. Both semantics are based on the minimality in the time distances of the existentially-quantified time events from the universally-quantified reference event, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small difference in the two semantics, for the strong minimal one, the TP problem is still undecidable, while for the weak minimal one, the TP problem is just PSPACE-complete. Membership in PSPACE is determined by exploiting a strictly more expressive extension (ECA\(^+\)) of the well-known robust class of Event-Clock Automata (ECA) that allows to encode the weak minimal TP problem and to reduce it to non-emptiness of Timed Automata (TA). Finally, an extension of ECA\(^+\) (ECA\(^{++}\)) is considered, proving that its non-emptiness problem is undecidable. We believe that the two extensions of ECA (ECA\(^+\) and ECA\(^{++}\)), introduced for technical reasons, are actually valuable per sé in the field of TA.
For the entire collection see [Zbl 1434.68021].