research-article

Open access

Partial-order Reduction Techniques for Real-time Model Checking

Authors:

Dennis Dams,

Rob Gerth,

Bart Knaack,

Ruurd KuiperAuthors Info & Claims

Formal Aspects of Computing, Volume 10, Issue 5

Pages 469 - 482

https://doi.org/10.1007/s001650050028

Published: 01 May 1998 Publication History

PDF eReader

Abstract.

A new notion, covering, generalising independence is introduced. It enables improved effects of partial-order reduction techniques when applied to real-time systems. Furthermore, we formulate a number of locally checkable conditions for covering that can be used as the basis for a practical algorithm. Correctness is proven with respect to a chosen discretisation method.

Cited By

View all

Srivathsan B(2022)Reachability in timed automataACM SIGLOG News10.1145/3559736.35597389:3(6-28)Online publication date: 25-Aug-2022
https://dl.acm.org/doi/10.1145/3559736.3559738
Govind RHerbreteau FSrivathsan Walukiewicz I(2022)Abstractions for the local-time semantics of timed automata: a foundation for partial-order methodsProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533343(1-14)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533343
Bouyer PGastin PHerbreteau FSankur OSrivathsan B(2022)Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next?Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_2(16-42)Online publication date: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_2
Show More Cited By

Index Terms

Partial-order Reduction Techniques for Real-time Model Checking

Index terms have been assigned to the content through auto-classification.

Recommendations

Combining partial-order reduction and symbolic model checking to verify LTL properties
NFM'11: Proceedings of the Third international conference on NASA Formal methods

BDD-based symbolic techniques and partial-order reduction (POR) are two fruitful approaches to deal with the combinatorial explosion of model checking. Unfortunately, past experience has shown that BDD-based techniques do not work well for loosely-...
Partial-order reduction and trail improvement in directed model checking

In this paper we present work on trail improvement and partial-order reduction in the context of directed explicit-state model checking. Directed explicit-state model checking employs directed heuristic search algorithms such as A* or best-first search ...
Reduction from branching-time property verification of higher-order programs to HFL validity checking
PEPM 2019: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation

Various methods have recently been proposed for temporal property verification of higher-order programs. In those methods, however, either temporal properties were limited to linear-time ones, or target programs were limited to finite-data programs. In ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Formal Aspects of Computing Volume 10, Issue 5

May 1998

141 pages

ISSN:0934-5043

EISSN:1433-299X

Issue’s Table of Contents

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 May 1998

Published in FAC Volume 10, Issue 5

Author Tag

Keywords: Verification; Model checking; Partial-order reduction; Real time; Covering

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
50
Total Downloads

Downloads (Last 12 months)40
Downloads (Last 6 weeks)5

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Srivathsan B(2022)Reachability in timed automataACM SIGLOG News10.1145/3559736.35597389:3(6-28)Online publication date: 25-Aug-2022
https://dl.acm.org/doi/10.1145/3559736.3559738
Govind RHerbreteau FSrivathsan Walukiewicz I(2022)Abstractions for the local-time semantics of timed automata: a foundation for partial-order methodsProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533343(1-14)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533343
Bouyer PGastin PHerbreteau FSankur OSrivathsan B(2022)Zone-Based Verification of Timed Automata: Extrapolations, Simulations and What Next?Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-15839-1_2(16-42)Online publication date: 12-Sep-2022
https://dl.acm.org/doi/10.1007/978-3-031-15839-1_2
Larsen KMikučionis MMuñiz MSrba J(2020)Urgent Partial Order Reduction for Extended Timed AutomataAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_10(179-195)Online publication date: 19-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-59152-6_10
Austin MJohnson J(2018)Compositional Approach to Distributed System Behavior Modeling and Formal Validation of Infrastructure Operations with Finite State Automata: Application to Viewpoint-Driven Verification of Functionality in WaterwaysSystems10.3390/systems60100026:1(2)Online publication date: 12-Jan-2018
https://doi.org/10.3390/systems6010002
Bønneland FJensen PLarsen KMuñiz MSrba J(2018)Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed SystemsComputer Aided Verification10.1007/978-3-319-96145-3_28(527-546)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96145-3_28
Zhou XLi QZhao J(2012)A New Approach of Partial Order Reduction Technique for Parallel Timed Automata Model CheckingProceedings of the 2012 IEEE Sixth International Conference on Software Security and Reliability Companion10.1109/SERE-C.2012.45(158-167)Online publication date: 20-Jun-2012
https://dl.acm.org/doi/10.1109/SERE-C.2012.45
Olderog ESwaminathan M(2010)Layered Composition for Timed AutomataFormal Modeling and Analysis of Timed Systems10.1007/978-3-642-15297-9_18(228-242)Online publication date: 2010
https://doi.org/10.1007/978-3-642-15297-9_18
Malinowski JNiebert P(2010)SAT based bounded model checking with partial order semantics for timed automataProceedings of the 16th international conference on Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-642-12002-2_34(405-419)Online publication date: 20-Mar-2010
https://dl.acm.org/doi/10.1007/978-3-642-12002-2_34
Jianhua ZLinzhang WXuandong L(2008)A Partial Order Reduction Technique for Parallel Timed Automaton Model CheckingLeveraging Applications of Formal Methods, Verification and Validation10.1007/978-3-540-88479-8_19(262-276)Online publication date: 2008
https://doi.org/10.1007/978-3-540-88479-8_19
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Abstract.

Cited By

Index Terms

Recommendations

Combining partial-order reduction and symbolic model checking to verify LTL properties

Partial-order reduction and trail improvement in directed model checking

Reduction from branching-time property verification of higher-order programs to HFL validity checking

Comments

Information

Published In

Publisher

Publication History

Author Tag

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

PDF

eReader

Login options

Full Access

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations