LTL with the freeze quantifier and register automata

DOI10.1145/1507244.1507246zbMATH Open1351.68158OpenAlexW2177814128MaRDI QIDQ2946574FDOQ2946574

Authors: Stéphane 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

Recommendations

• Safely Freezing LTL
• On freeze LTL with ordered attributes
• Safety alternating automata on data words
• Future-Looking Logics on Data Words and Trees
• Alternating register automata on finite words and trees

zbMATH Keywords

computational complexityexpressiveness

Mathematics Subject Classification ID

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)

Cited In (73)

• A note on the emptiness problem for alternating finite-memory automata
• The Parametric Complexity of Lossy Counter Machines
• Synthesis of data word transducers
• Weak and nested class memory automata
• Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints
• Separation logics and modalities: a survey
• Reactive synthesis from visibly register pushdown automata
• Model checking memoryful linear-time logics over one-counter automata
• Path checking for MTL and TPTL over data words
• An automata-theoretic approach to constraint LTL
• Algorithmic Analysis of Array-Accessing Programs
• Automated program verification
• Nondeterministic and co-nondeterministic implies deterministic, for data languages
• Playing with Repetitions in Data Words Using Energy Games
• Reachability in pushdown register automata
• Adding one or more equivalence relations to the interval temporal logic \(\mathsf{AB}\overline{\mathsf{B}}\)
• An automaton over data words that captures EMSO logic
• Timeline-based planning over dense temporal domains
• Trace inclusion for one-counter nets revisited
• Temporal logics of repeating values
• Title not available (Why is that?)
• Selective monitoring
• Logics of repeating values on data trees and branching counter systems
• Active learning for deterministic bottom-up nominal tree automata
• Title not available (Why is that?)
• Metric propositional neighborhood logic with an equivalence relation
• Future-Looking Logics on Data Words and Trees
• The containment problem for unambiguous register automata
• Weighted register automata and weighted logic on data words
• Weighted register automata and weighted logic on data words
• The containment problem for unambiguous register automata and unambiguous timed automata
• Trace inclusion for one-counter nets revisited
• Streamable regular transductions
• Process-centric views of data-driven business artifacts
• Satisfiability of \(\mathrm{ECTL}^*\) with local tree constraints
• Expressiveness of hybrid temporal logic on data words
• On temporal logics with data variable quantifications: decidability and complexity
• Extending two-variable logic on data trees with order on data values and its automata
• Complexity results on register context-free grammars and related formalisms
• On the termination and structural termination problems for counter machines with incrementing errors
• A taxonomy and reductions for common register automata formalisms
• Regular expressions for data words
• Branching-time logics repeatedly referring to states
• Linear-time temporal logic with event freezing functions
• Title not available (Why is that?)
• First-order \(\mu\)-calculus over generic transition systems and applications to the situation calculus
• Computable fixpoints in well-structured symbolic model checking
• SMT-based satisfiability of first-order LTL with event freezing functions and metric operators
• Reactive synthesis from interval temporal logic specifications
• Complexity hierarchies beyond elementary
• Model-Checking Counting Temporal Logics on Flat Structures
• Safety alternating automata on data words
• On computability of data word functions defined by transducers
• Ordered navigation on multi-attributed data words
• On freeze LTL with ordered attributes
• Nominal automata with name binding
• A class of automata for the verification of infinite, resource-allocating behaviours
• On pebble automata for data languages with decidable emptiness problem
• Temporal stream logic modulo theories
• Title not available (Why is that?)
• Church synthesis on register automata over linearly ordered data domains
• Title not available (Why is that?)
• Realizability problem for constraint LTL
• A Note on C² Interpreted over Finite Data-Words
• Set augmented finite automata over infinite alphabets
• Universality Problem for Unambiguous VASS
• Model checking flat Freeze LTL on one-counter automata
• Title not available (Why is that?)
• The complexity of flat freeze LTL
• The complexity of flat freeze LTL
• Optimal run problem for weighted register automata
• $$\textsc {Reach}$$ on Register Automata via History Independence
• Reasoning on data words over numeric domains

This page was built for publication: LTL with the freeze quantifier and register automata

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