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

• Systems and software verification. Model-checking techniques and tools
• 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 survey of regular model checking
• 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
• From linear temporal logics to Büchi automata: the early and simple principle
• Handling global conditions in parameterized system verification
• High-level representation of benchmark families for Petri games
• Incremental requirement specification for evolving systems
• Inferring canonical register automata
• Never-stop context-free learning
• On the correspondence between conformance testing and regular inference
• Quantitative analysis of interval Markov chains
• Regular model checking
• Regular model checking revisited
• Regular tree model checking
• Transitive closures of regular relations for verifying infinite-state systems

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)