Deciding properties of integral relational automata

DOI10.1007/3-540-58201-0_56zbMath1418.68126OpenAlexW2146250272MaRDI QIDQ4632414

Kārlis Čerāns

Publication date: 29 April 2019

Published in: Automata, Languages and Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-58201-0_56

zbMATH Keywords

timed automatamodel checkinglinear-time temporal logicinequality system

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items (15)

Satisfiability of \(\operatorname{ECTL}^\ast\) with constraints ⋮ An automata-theoretic approach to constraint LTL ⋮ Verification of gap-order constraint abstractions of counter systems ⋮ Deciding properties of integral relational automata ⋮ Computable fixpoints in well-structured symbolic model checking ⋮ Verification of qualitative \(\mathbb Z\) constraints ⋮ An Automata-based Approach for CTL⋆ With Constraints ⋮ A classification of the expressive power of well-structured transition systems ⋮ Well-structured transition systems everywhere! ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ LTL over integer periodicity constraints ⋮ Data Multi-Pushdown Automata ⋮ Model checking of systems with many identical timed processes ⋮ Algorithmic analysis of programs with well quasi-ordered domains. ⋮ CTL* model checking for data-aware dynamic systems with arithmetic

Cites Work

• Undecidable verification problems for programs with unreliable channels
• The complementation problem for Büchi automata with applications to temporal logic
• Automata-theoretic techniques for modal logics of programs
• Bisimulation equivalence is decidable for all context-free processes
• Verifying programs with unreliable channels
• An Algorithm for the General Petri Net Reachability Problem
• Automatic verification of finite-state concurrent systems using temporal logic specifications
• Automatic construction of test sets: Theoretical approach
• Deciding properties of integral relational automata
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Deciding properties of integral relational automata