scientific article; zbMATH DE number 7649960

DOI10.4230/LIPIcs.ITP.2019.11MaRDI QIDQ5875419

Julian Brunner, Salomon Sickert, Benedikt Seidl

Publication date: 3 February 2023

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

zbMATH Keywords

automata theorymodel checkinglinear temporal logicdeterministic automataautomata over infinite wordsverified algorithms

Mathematics Subject Classification ID

Related Items (1)

Certifying emptiness of timed Büchi automata

Uses Software

• Isabelle/HOL
• SPOT
• LTL2BA
• Locales
• Autoref
• Transfer
• Lifting
• Refinement Monadic
• Archive Formal Proofs
• Boolean_Expression_Checkers

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formal verification of an executable LTL model checker with partial order reduction
• Isabelle/HOL. A proof assistant for higher-order logic
• Verifying the LTL to Büchi automata translation via very weak alternating automata
• Locales: a module system for mathematical theories
• From LTL to deterministic automata. A safraless compositional approach
• Truly Modular (Co)datatypes for Isabelle/HOL
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Unified Decision Procedures for Regular Expression Equivalence
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
• Structured Formal Development with Quotient Types in Isabelle/HOL
• The complexity of probabilistic verification
• Handbook of Model Checking
• Limit-Deterministic Büchi Automata for Linear Temporal Logic
• One Theorem to Rule Them All
• Effective Translation of LTL to Deterministic Rabin Automata: Beyond the (F,G)-Fragment
• Derivatives of Regular Expressions

This page was built for publication: