An approximation-based incremental SMT approach for diagnosability analysis of real-time systems

DOI10.1007/S10626-025-00420-XMaRDI QIDQ6912384zbMATH OpenFDO

Authors Lulu He, Philippe Dague, Lina Ye

Publication date 22 October 2025

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/S10626-025-00420-X

zbMATH Keywords

approximationscounterexample-guided abstraction refinement (CEGAR)diagnosabilitysatisfiability modulo theories (SMT)timed automata

Mathematics Subject Classification ID

Discrete event control/observation systems (93C65)

Cites work

• A polynomial algorithm for testing diagnosability of discrete-event systems
• A theory of timed automata
• Abstraction refinement algorithms for timed automata
• Abstractions Refinement for Hybrid Systems Diagnosability Analysis
• Active diagnosis of discrete-event systems
• Automatic Abstraction Refinement for Timed Automata
• Diagnosability of discrete-event systems
• Exact Incremental Analysis of Timed Automata with an SMT-Solver
• Fault diagnosis for timed automata
• Foundations of Software Science and Computational Structures
• scientific article; zbMATH DE number 1670775 (Why is no real title available?)
• Predictability of event occurrences in partially-observed discrete-event systems
• SAT-based reachability checking for timed automata with discrete data

This page was built for publication: An approximation-based incremental SMT approach for diagnosability analysis of real-time systems

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