SMT-based model checking of max-plus linear systems

DOI10.4230/LIPICS.CONCUR.2021.22MaRDI QIDQ6134268zbMATH OpenOpenAlexFDO

Authors Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, Alessandro Cimatti

Publication date 21 August 2023

Full work available at URL https://doi.org/10.4230/LIPIcs.CONCUR.2021.22

zbMATH Keywords

linear temporal logicmax-plus linear systemsmodel checkingsatisfiability modulo theory

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Bounded model checking of max-plus linear systems via predicate abstractions
• SMT-Based Reachability Analysis of High Dimensional Interval Max-Plus Linear Systems
• Formal Verification of Stochastic Max-Plus-Linear Systems
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Computation of the transient in max-plus linear systems via SMT-solving
• scientific article; zbMATH DE number 1903366
• Model checking of linear-time properties in multi-valued systems

This page was built for publication: SMT-based model checking of max-plus linear systems

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