Model checking, synthesis, and learning

DOI10.1007/978-3-030-91384-7_1zbMATH Open1522.68339OpenAlexW4206152085MaRDI QIDQ6041187FDOQ6041187

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

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

zbMATH Keywords

verificationMarkov chainsPetri netsprobabilistic systemstimed systemsregister automatalinear-time temporal logicmodel synthesisautomata learningPetri gamesBüchi automata(regular) model checking

Mathematics Subject Classification ID

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

Cites Work

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

Cited In (2)

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

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)