Using non-convex approximations for efficient analysis of timed automata

DOI10.4230/LIPICS.FSTTCS.2011.78MaRDI QIDQ2911614zbMATH OpenFDO

Authors Frédéric Herbreteau, Dileep Kini, B. Srivathsan, Igor Walukiewicz

Publication date 31 August 2012

Full work available at URL https://arxiv.org/abs/1110.3704

zbMATH Keywords

model checkingnon-convex abstractionon-the-fly abstractiontimed automata

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Better abstractions for timed automata
• Lazy reachability checking for timed automata using interpolants
• Better abstractions for timed automata
• On Interleaving in Timed Automata
• Dynamical Properties of Timed Automata Revisited

Cited in

(13)

• Configurable verification of timed automata with discrete variables
• Model-based verification, optimization, synthesis and performance evaluation of real-time systems
• Better abstractions for timed automata
• Exact Incremental Analysis of Timed Automata with an SMT-Solver
• Better abstractions for timed automata
• Hypervolume Approximation in Timed Automata Model Checking
• Robust reachability in timed automata and games: a game-based approach
• Reachability in timed automata with diagonal constraints
• Lazy Reachability Checking for Timed Automata with Discrete Variables
• Fast algorithms for handling diagonal constraints in timed automata
• Dense integer-complete synthesis for bounded parametric timed automata
• Parameterized verification of timed networks with clock invariants
• Fast zone-based algorithms for reachability in pushdown timed automata

Describes a project that uses

Uses Software

• POEM
• Uppaal

This page was built for publication: Using non-convex approximations for efficient analysis of timed automata

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