LTL with the freeze quantifier and register automata
From MaRDI portal
Publication:2946574
DOI10.1145/1507244.1507246zbMath1351.68158OpenAlexW2177814128MaRDI QIDQ2946574
Stéphane P. Demri, Ranko Lazić
Publication date: 17 September 2015
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/1507244.1507246
Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)
Related Items (68)
Reactive synthesis from visibly register pushdown automata ⋮ Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\) ⋮ Trace Inclusion for One-Counter Nets Revisited ⋮ Path Checking for MTL and TPTL over Data Words ⋮ Weighted Register Automata and Weighted Logic on Data Words ⋮ Trace inclusion for one-counter nets revisited ⋮ Future-Looking Logics on Data Words and Trees ⋮ Metric propositional neighborhood logic with an equivalence relation ⋮ On temporal logics with data variable quantifications: decidability and complexity ⋮ Reachability in pushdown register automata ⋮ Process-centric views of data-driven business artifacts ⋮ An automata-theoretic approach to constraint LTL ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints ⋮ Unnamed Item ⋮ SMT-based satisfiability of first-order LTL with event freezing functions and metric operators ⋮ Complexity results on register context-free grammars and related formalisms ⋮ Separation logics and modalities: a survey ⋮ A taxonomy and reductions for common register automata formalisms ⋮ Set augmented finite automata over infinite alphabets ⋮ Active learning for deterministic bottom-up nominal tree automata ⋮ Temporal stream logic modulo theories ⋮ Church synthesis on register automata over linearly ordered data domains ⋮ Unnamed Item ⋮ Realizability problem for constraint LTL ⋮ On computability of data word functions defined by transducers ⋮ Unnamed Item ⋮ First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus ⋮ A note on the emptiness problem for alternating finite-memory automata ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On pebble automata for data languages with decidable emptiness problem ⋮ Nominal Automata with Name Binding ⋮ Logics of Repeating Values on Data Trees and Branching Counter Systems ⋮ Unnamed Item ⋮ Nondeterministic and co-nondeterministic implies deterministic, for data languages ⋮ Timeline-based planning over dense temporal domains ⋮ A Note on C² Interpreted over Finite Data-Words ⋮ Extending two-variable logic on data trees with order on data values and its automata ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Model checking memoryful linear-time logics over one-counter automata ⋮ Unnamed Item ⋮ Weighted register automata and weighted logic on data words ⋮ Playing with Repetitions in Data Words Using Energy Games ⋮ Unnamed Item ⋮ Automated Program Verification ⋮ Weak and Nested Class Memory Automata ⋮ Streamable regular transductions ⋮ On the termination and structural termination problems for counter machines with incrementing errors ⋮ On Freeze LTL with Ordered Attributes ⋮ Optimal run problem for weighted register automata ⋮ A Class of Automata for the Verification of Infinite, Resource-Allocating Behaviours ⋮ The containment problem for unambiguous register automata and unambiguous timed automata ⋮ An Automaton over Data Words That Captures EMSO Logic ⋮ Universality Problem for Unambiguous VASS ⋮ The Containment Problem for Unambiguous Register Automata ⋮ Expressiveness of Hybrid Temporal Logic on Data Words ⋮ Reactive synthesis from interval temporal logic specifications ⋮ The Parametric Complexity of Lossy Counter Machines ⋮ Complexity Hierarchies beyond Elementary ⋮ Algorithmic Analysis of Array-Accessing Programs ⋮ Unnamed Item ⋮ The Complexity of Flat Freeze LTL ⋮ Model-Checking Counting Temporal Logics on Flat Structures ⋮ Branching-time logics repeatedly referring to states ⋮ Regular expressions for data words
This page was built for publication: LTL with the freeze quantifier and register automata
