Model checking, synthesis, and learning

DOI10.1007/978-3-030-91384-7_1MaRDI QIDQ6041187zbMATH OpenOpenAlexFDO

Authors Ernst-Rüdiger Olderog, Bernhard Steffen, Wang Yi

Publication date 26 May 2023

Published in Model Checking, Synthesis, and Learning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-030-91384-7_1

zbMATH Keywords

(regular) model checkingautomata learningBüchi automatalinear-time temporal logicMarkov chainsmodel synthesisPetri gamesPetri netsprobabilistic systemsregister automatatimed systemsverification

Mathematics Subject Classification ID

Computational learning theory (68Q32) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• scientific article; zbMATH DE number 1633145
• Software reliability methods. Foreword by Edmund M. Clarke
• Software model checking
• scientific article; zbMATH DE number 5585443
• Formal models for software development. Model checking, verification, analysis and simulation

Cites work

• A logic for reasoning about time and reliability
• A Succinct Canonical Register Automaton Model
• A succinct canonical register automaton model for data domains with binary relations
• A taxonomy and reductions for common register automata formalisms
• Active learning for extended finite state machines
• Algorithmic improvements in regular model checking.
• Assumption/guarantee specifications in linear-time temporal logic
• Combining black-box and white-box techniques for learning register automata
• CONCUR 2004 - Concurrency Theory
• From linear temporal logics to Büchi automata: the early and simple principle
• Fundamental Approaches to Software Engineering
• High-level representation of benchmark families for Petri games
• scientific article; zbMATH DE number 1670791 (Why is no real title available?)
• scientific article; zbMATH DE number 1538041 (Why is no real title available?)
• scientific article; zbMATH DE number 1903380 (Why is no real title available?)
• scientific article; zbMATH DE number 2102701 (Why is no real title available?)
• Incremental requirement specification for evolving systems
• Inferring canonical register automata
• Never-stop context-free learning
• Quantitative analysis of interval Markov chains
• Regular model checking revisited

Cited in

(2)

• Interpolant learning and reuse in SAT-based model checking
• Synchronous or alternating? LTL black-box checking of Mealy machines by combining the LearnLib and LTSmin

This page was built for publication: Model checking, synthesis, and learning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6041187)