Reachability analysis for timed automata using max-plus algebra

DOI10.1016/J.JLAP.2011.10.004MaRDI QIDQ444476zbMATHOpenAlexWikidataFDO

Authors Qi Lu, Michael Madsen, Martin Milata, Uli Fahrenberg, Søren Ravn, Kim G. Larsen

Publication date 14 August 2012

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2011.10.004

zbMATH Keywords

data structuremax-plus algebramax-plus polyhedronreal-time model checkingtimed automaton

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Data structures (68P05) Max-plus and related algebras (15A80) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Computational techniques for reachability analysis of Max-Plus-Linear systems
• scientific article; zbMATH DE number 2144766
• Size-Change Abstraction and Max-Plus Automata
• scientific article; zbMATH DE number 2064231
• scientific article; zbMATH DE number 1670871

Cites work

• scientific article; zbMATH DE number 177824 (Why is no real title available?)
• scientific article; zbMATH DE number 3570223 (Why is no real title available?)
• scientific article; zbMATH DE number 1948398 (Why is no real title available?)
• scientific article; zbMATH DE number 1738295 (Why is no real title available?)
• scientific article; zbMATH DE number 2102717 (Why is no real title available?)
• scientific article; zbMATH DE number 1400094 (Why is no real title available?)
• scientific article; zbMATH DE number 1424030 (Why is no real title available?)
• A theory of timed automata
• Correctness kernels of abstract interpretations
• Formal Modeling and Analysis of Timed Systems
• Generators, extremals and bases of max cones
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Kronos: A verification tool for real-time systems
• Reachability analysis for timed automata using max-plus algebra
• Reactive Systems
• Static Analysis in Disjunctive Numerical Domains
• Symbolic model checking for real-time systems
• The Minkowski theorem for max-plus convex sets
• The octagon abstract domain
• The tropical double description method
• Tools and Algorithms for the Construction and Analysis of Systems
• Verification, performance analysis and controller synthesis for real-time systems

Cited in

(14)

• Performance evaluation of (max,+) automata
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• On the set-estimation of uncertain max-plus linear systems
• Tropical Fourier-Motzkin elimination, with an application to real-time verification
• Decoupled fitness criteria for reactive systems
• Analysis and control of max-plus linear discrete-event systems: an introduction
• scientific article; zbMATH DE number 1670871 (Why is no real title available?)
• Reachability analysis for timed automata using max-plus algebra
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Optimal time-bounded reachability analysis for concurrent systems
• On the complexity of strongly connected components in directed hypergraphs
• Conditional reachability of uncertain max plus linear systems
• Formal analysis and control of timed automata with guards using (max, +) and (min, +) algebras
• Fault localization of timed automata using maximum satisfiability

Describes a project that uses

Uses Software

• Kronos
• PPL
• Octagon
• Algorithm 97

This page was built for publication: Reachability analysis for timed automata using max-plus algebra

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