scientific article; zbMATH DE number 1796123

Publication date: 4 September 2002

Full work available at URL: http://link.springer.de/link/service/series/0558/bibs/2102/21020053

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

From LTL to deterministic automata. A safraless compositional approach ⋮ LTL receding horizon control for finite deterministic systems ⋮ Translating Testing Theories for Concurrent Systems ⋮ Efficient approach of translating LTL formulae into Büchi automata ⋮ Automata Theory and Model Checking ⋮ The mu-calculus and Model Checking ⋮ Graph Games and Reactive Synthesis ⋮ Extending Co-logic Programs for Branching-Time Model Checking ⋮ Multi-Valued Reasoning about Reactive Systems ⋮ From LTL to unambiguous Büchi automata via disambiguation of alternating automata ⋮ Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL ⋮ Degeneralization algorithm for generation of Büchi automata based on contented situation ⋮ On clock-aware LTL parameter synthesis of timed automata ⋮ Experiments with deterministic \(\omega\)-automata for formulas of linear temporal logic ⋮ Logic programming approach to automata-based decision procedures ⋮ LTL Parameter Synthesis of Parametric Timed Automata ⋮ Verifying a signature architecture: a comparative case study ⋮ Safraless LTL synthesis considering maximal realizability ⋮ Resource-aware networked control systems under temporal logic specifications ⋮ Path planning for robotic teams based on LTL specifications and Petri net models ⋮ Temporal logic guided safe model-based reinforcement learning: a hybrid systems approach ⋮ Minimal counterexamples for linear-time probabilistic verification ⋮ On-the-Fly Stuttering in the Construction of Deterministic ω-Automata ⋮ A canonical form based decision procedure and model checking approach for propositional projection temporal logic ⋮ From LTL to rLTL monitoring: improved monitorability through robust semantics ⋮ Model checking of pushdown systems for projection temporal logic ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ Unnamed Item ⋮ Energy Büchi problems ⋮ SySCoRe: Synthesis via Stochastic Coupling Relations ⋮ LTL to self-loop alternating automata with generic acceptance and back ⋮ Unnamed Item ⋮ Automated temporal equilibrium analysis: verification and synthesis of multi-player games ⋮ Temporal property verification as a program analysis task ⋮ Symbolic bounded synthesis ⋮ Linear temporal logic symbolic model checking ⋮ Runtime verification using the temporal description logic \(\mathcal{ALC}\)-LTL revisited ⋮ New Optimizations and Heuristics for Determinization of Büchi Automata ⋮ Approximate Automata for Omega-Regular Languages ⋮ Büchi Store: An Open Repository of Büchi Automata ⋮ Unbeast: Symbolic Bounded Synthesis ⋮ A compositional automata-based semantics and preserving transformation rules for testing property patterns ⋮ Component-wise incremental LTL model checking ⋮ Coinductive Algorithms for Büchi Automata ⋮ Parametric linear dynamic logic ⋮ The modeling library of eavesdropping methods in quantum cryptography protocols by model checking ⋮ Unnamed Item ⋮ An Automata View to Goal-Directed Methods ⋮ From Philosophical to Industrial Logics ⋮ Model Checking LTL Formulae in RAISE with FDR ⋮ Analog property checkers: a DDR2 case study ⋮ Unnamed Item ⋮ From Monadic Logic to PSL ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ Automata-Theoretic Model Checking Revisited ⋮ From LTL to Symbolically Represented Deterministic Automata ⋮ Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking ⋮ GOAL Extended: Towards a Research Tool for Omega Automata and Temporal Logic ⋮ Mediating for reduction (on minimizing alternating Büchi automata) ⋮ Tool support for learning Büchi automata and linear temporal logic ⋮ On-the-fly Emptiness Check of Transition-Based Streett Automata ⋮ On the Relationship between LTL Normal Forms and Büchi Automata ⋮ More efficient on-the-fly LTL verification with Tarjan's algorithm

Uses Software