Bounded model-checking of discrete duration calculus

DOI10.1145/2461328.2461362MaRDI QIDQ2986927zbMATH OpenOpenAlexFDO

Authors Quan Zu, Miaomiao Zhang, Jiaqi Zhu, Naijun Zhan

Publication date 16 May 2017

Published in Proceedings of the 16th international conference on Hybrid systems: computation and control (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2461328.2461362

zbMATH Keywords

hybrid systemsmodel checkingtimed automataduration calculus

Mathematics Subject Classification ID

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

Recommendations

• Take It NP-Easy: Bounded Model Construction for Duration Calculus
• A practical approach to model checking duration calculus using Presburger arithmetic
• Model-checking discrete duration calculus
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Bounded model checking for timed automata

Cites work

• scientific article; zbMATH DE number 5595151 (Why is no real title available?)
• scientific article; zbMATH DE number 2080065 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A Fully Automated Framework for Control of Linear Systems from Temporal Logic Specifications
• A note on two problems in connexion with graphs
• Controlling a Class of Nonlinear Systems on Rectangles
• Diagnostic Information for Realizability
• Enhancing model checking in verification by AI techniques
• Markov decision processes and regular events
• Model repair for probabilistic systems
• Receding horizon control for temporal logic specifications

Cited in

(12)

• A practical approach to model checking duration calculus using Presburger arithmetic
• Model checking bounded continuous-time extended linear duration invariants
• Formal Modeling and Analysis of Timed Systems
• Checking MTL Properties of Discrete Timed Automata via Bounded Model Checking
• Take It NP-Easy: Bounded Model Construction for Duration Calculus
• Tools and Algorithms for the Construction and Analysis of Systems
• Model-checking dense-time duration calculus
• scientific article; zbMATH DE number 2087436 (Why is no real title available?)
• Finding extremal models of discrete duration calculus formulae using symbolic search
• Bounded model checking distributed temporal logic
• Model-checking discrete duration calculus
• Bounded model checking for timed automata

Describes a project that uses

Uses Software

• DCVALID
• Uppaal

This page was built for publication: Bounded model-checking of discrete duration calculus

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