Reachability analysis for timed automata using max-plus algebra

DOI10.1016/j.jlap.2011.10.004zbMath1279.68214OpenAlexW2109586922WikidataQ114851545 ScholiaQ114851545MaRDI QIDQ444476

Qi Lu, Michael Madsen, Martin Milata, Uli Fahrenberg, Søren Hove Ravn, Kim Guldstrand 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

max-plus algebradata structuremax-plus polyhedronreal-time model checkingtimed automaton

Mathematics Subject Classification ID

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

Related Items (7)

Tropical Fourier–Motzkin elimination, with an application to real-time verification ⋮ Analysis and control of max-plus linear discrete-event systems: an introduction ⋮ Computational techniques for reachability analysis of Max-Plus-Linear systems ⋮ Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems ⋮ Reachability analysis for timed automata using max-plus algebra ⋮ On the complexity of strongly connected components in directed hypergraphs ⋮ Conditional reachability of uncertain max plus linear systems

Uses Software

• Kronos
• PPL
• Octagon
• Algorithm 97

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Reachability analysis for timed automata using max-plus algebra
• The octagon abstract domain
• The Minkowski theorem for max-plus convex sets
• Generators, extremals and bases of max cones
• A theory of timed automata
• Symbolic model checking for real-time systems
• Kronos: A verification tool for real-time systems
• Correctness kernels of abstract interpretations
• Verification, Performance Analysis and Controller Synthesis for Real-Time Systems
• Inferring Min and Max Invariants Using Max-Plus Polyhedra
• Static Analysis in Disjunctive Numerical Domains
• Tools and Algorithms for the Construction and Analysis of Systems
• Reactive Systems
• Formal Modeling and Analysis of Timed Systems

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