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

design toolformal specification and verificationmodel checkingreal-time systemstimed automata

Mathematics Subject Classification ID

Data structures (68P05) Formal languages and automata (68Q45) 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)

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

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)