Certifying emptiness of timed Büchi automata
type: Item
instance of: scholarly article
title: Certifying emptiness of timed Büchi automata
DOI: 10.1007/978-3-030-57628-8_4
author: Simon Wimmer
author: Frédéric Herbreteau
author: Jaco van de Pol
publication date: 2021-03-02T00:00:00Z
full work available at URL: https://arxiv.org/abs/2007.04150
full work available at URL: certifying-emptiness-of-timed-buchi-automata(f54af37b-48b1-4208-a9ff-80291711cf20).html
Mathematics Subject Classification ID: 68Qxx
zbMATH DE Number: 7317090
zbMATH Keywords: timed automata
zbMATH Keywords: certification
zbMATH Keywords: model checking
describes a project that uses: Isabelle/HOL
MaRDI profile type: Publication
OpenAlex ID: W3082487236
cites work: A theory of timed automata
cites work: Synthesis of Timing Parameters Satisfying Safety Properties
cites work: Q4417927
cites work: Lectures on Concurrency and Petri Nets
cites work: A verified SAT solver framework with learn, forget, restart, and incrementality
cites work: Formal verification of an executable LTL model checker with partial order reduction
cites work: Q5875419
cites work: Well-structured transition systems everywhere!
cites work: Why Liveness for Timed Automata Is Hard, and What We Can Do About It
cites work: Better abstractions for timed automata
cites work: Efficient, verified checking of propositional proofs
cites work: Efficient verified (UN)SAT certificate checking
cites work: Uppaal in a nutshell
cites work: Checking Timed Büchi Automata Emptiness Using LU-Abstractions
cites work: Q4553254
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Automated Verification of Parallel Nested DFS
cites work: Checking timed Büchi automata emptiness on simulation graphs
cites work: Checking timed Büchi automata emptiness efficiently
cites work: Verified model checking of timed automata
cites work: Verified Certification of Reachability Checking for Timed Automata
description: scientific article; zbMATH DE number 7317090