An optimal pastification algorithm for LTL X, F and LTL X, G

DOI10.1016/J.ARTINT.2026.104553MaRDI QIDQ7304002zbMATH OpenFDO

Authors Alessandro Artale, Luca Geatti, Nicola Gigante, Alessio Mansutti, Angelo Montanari

Publication date 24 July 2026

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/J.ARTINT.2026.104553

Mathematics Subject Classification ID

Temporal logic (03B44) Logic in artificial intelligence (68T27)

Cites work

• Algebraic Theory of Machines. I. Prime Decomposition Theorem for Finite Semigroups and Machines
• Analysis of timed systems using time-abstracting bisimulations
• Characterization of temporal property classes
• Extended bounded response LTL: a new safety fragment for efficient reactive synthesis
• Fault diagnosis for timed automata
• scientific article; zbMATH DE number 3368555 (Why is no real title available?)
• Model checking of safety properties
• On cascades of reset automata
• On the Krohn-Rhodes cascaded decomposition theorem
• Past is for free: On the complexity of verifying linear temporal properties with past
• SAT meets tableaux for linear temporal logic satisfiability
• Separation -- past, present, and future
• Succinctness issues for \(\textsf{LTL}_{\textsf{f}}\) and safety and cosafety fragments of \textsf{LTL}
• Succinctness of cosafety fragments of LTL via combinatorial proof systems
• The complexity of propositional linear temporal logics

This page was built for publication: An optimal pastification algorithm for \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{F} \rbrack\) and \(\mathsf{LTL} \lbrack \mathsf{X}, \mathsf{G} \rbrack \)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7304002)