Compact data structures and state-space reduction for model-checking real-time systems

DOI10.1023/A:1025132427497MaRDI QIDQ1431366zbMATH OpenOpenAlexFDO

Authors Fredrik Larsson, Paul Pettersson, Wang Yi, Kim G. Larsen

Publication date 27 May 2004

Published in Real-Time Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1023/a:1025132427497

zbMATH Keywords

model checkingreal-time systemstimed automatadesign toolformal specification and verification

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 2102717
• Model-checking for real-time systems
• Formal Modeling and Analysis of Timed Systems
• A space-efficient on-the-fly algorithm for real-time model checking
• To store or not to store.

Cited in

(10)

• Inference in probabilistic logic programs using lifted explanations
• Formal verification of multitasking applications based on timed automata model
• Model checking time-dependent system specifications using time stream Petri nets and \texttt{UPPAAL}
• To store or not to store.
• Data constraints for validation of real-time software
• scientific article; zbMATH DE number 1629960 (Why is no real title available?)
• Abstractions for the local-time semantics of timed automata: a foundation for partial-order methods
• scientific article; zbMATH DE number 2102717 (Why is no real title available?)
• Model-checking precision agriculture logistics: the case of the differential harvest
• scientific article; zbMATH DE number 1629959 (Why is no real title available?)

Describes a project that uses

Uses Software

• Uppaal

This page was built for publication: Compact data structures and state-space reduction for model-checking real-time systems

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