scientific article; zbMATH DE number 7649960
From MaRDI portal
Publication:5875419
automata over infinite wordsautomata theorydeterministic automatalinear temporal logicmodel checkingverified algorithms
Cites work
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Derivatives of Regular Expressions
- Effective translation of LTL to deterministic Rabin automata: beyond the \((\mathrm F,\mathrm G)\)-fragment
- Formal verification of an executable LTL model checker with partial order reduction
- From LTL to deterministic automata. A safraless compositional approach
- Handbook of model checking
- scientific article; zbMATH DE number 1670757 (Why is no real title available?)
- scientific article; zbMATH DE number 1796123 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Limit-deterministic Büchi automata for linear temporal logic
- Locales: a module system for mathematical theories
- One theorem to rule them all: a unified translation of LTL into -automata
- Structured formal development with quotient types in Isabelle/HOL
- The complexity of probabilistic verification
- Truly modular (co)datatypes for Isabelle/HOL
- Unified decision procedures for regular expression equivalence
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Verifying the LTL to Büchi automata translation via very weak alternating automata
Cited in
(4)
Describes a project that uses
Uses Software
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875419)
