research-article

Model Checking Bounded Continuous-time Extended Linear Duration Invariants

Authors:

Miaomiao Zhang,

Wang YiAuthors Info & Claims

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

Pages 81 - 90

https://doi.org/10.1145/3178126.3178147

Published: 11 April 2018 Publication History

Abstract

Extended Linear Duration Invariants (ELDI), an important subset of Duration Calculus, extends well-studied Linear Duration Invariants with logical connectives and the chop modality. It is known that the model checking problem of ELDI is undecidable with both the standard continuous-time and discrete-time semantics [12, 13], but it turns out to be decidable if only bounded execution fragments of timed automata are concerned in the context of the discrete-time semantics [36]. In this paper, we prove that this problem is still decidable in the continuous-time semantics, although it is well-known that model-checking Duration Calculus with the continuous-time semantics is much more complicated than the one with the discrete-time semantics. This is achieved by reduction to the validity of Quantified Linear Real Arithmetic (QLRA). Some examples are provided to illustrate the efficiency of our approach.

References

[1]

R. Alur and D. L. Dill. 1994. A theory of timed automata. TCS 126(2) (1994), 183--235.

Digital Library

[2]

J. Bengtsson and Y. Wang. 2004. Timed Automata: Semantics, Algorithms and Tools. In Lectures on Concurrency and Petri Nets: Advances in Petri Nets. 87--124.

[3]

V. A. Braberman and D. V. Huang. 1998. On checking timed automata for linear duration invariants. In RTSS 1998. 264 - 273.

Digital Library

[4]

C. W. Brown. 2003. QEPCAD B: A program for computing with semialgebraic sets using CADs. ACM SIGSAM Bulletin 37, 4 (2003), 97--108.

Digital Library

[5]

G. Collins. 1975. Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In 2nd GI Conference on Automata Theory and Formal Languages. 134--183.

Digital Library

[6]

W. Damm, M. Horbach, and V. Sofronie-Stokkermans. 2015. Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata. In FroCoS 2015. 186--202.

Digital Library

[7]

W. Damm, C. Ihlemann, and V. Sofronie-Stokkermans. 2011. Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata. In HSCC 2011. 73--82.

Digital Library

[8]

A. Dolzmann, A. Seidl, and T. Sturm. 2006. Redlog User Manual (Edition 3.1, for Redlog Version 3.06 (Reduce 3.8) ed.).

[9]

A. Dolzmann, T. Sturm, and V. Weispfenning. 1998. A new approach for automatic theorem proving in real geometry. J. of Automated Reasoning 21, 3 (1998), 357--380.

Digital Library

[10]

M. Fränzle. 2004. Model-checking dense-time Duration Calculus. Formal Aspects of Computing 16, 2 (2004), 121--139.

[11]

M. Fränzle and M. R. Hansen. 2007. Deciding an interval logic with accumulated durations. In TACAS 2007. 201--215.

Digital Library

[12]

M. Fränzle and M. R. Hansen. 2008. Efficient model checking for Duration Calculus based on branching-time approximations. In SEFM 2008. 63--72.

Digital Library

[13]

M. Fränzle and M. R. Hansen. 2009. Efficient model checking for duration calculus. International Journal of Software and Informatics 3, 2-3 (2009), 171--196.

[14]

V. Goranko, A. Montanari, and G. Sciavicco. 2004. A road map of interval temporal logics and duration calculi. J. of Applied Non-Classical Logics 14, 1-2 (2004), 9--54.

[15]

J. Y. Halpern, Z. Manna, and B. C. Moszkowski. 1983. A hardware semantics based on temporal intervals. In ICALP 1983. 278--291.

Digital Library

[16]

M. R. Hansen. 1994. Model-checking discrete Duration Calculus. Formal Aspects of Computing 6, 1 (1994), 826--845.

[17]

T. A. Henzinger. 1996. The theory of hybrid automata. In LICS 1996. 278--292.

Digital Library

[18]

C. Zhou. C. A. R. Hoare and A. P. Ravn. 1991. A calculus of durations. Inf. Proc. Let. 40, 5 (1991), 269--276.

[19]

K. G. Larsen, P. Pettersson, and Y. Wang. 1997. Uppaal in a nutshell. STTT 1, 1 (1997), 134--152.

Digital Library

[20]

X. Li. and D. V. Huang. 1996. Checking linear duration invariants by linear programming. In ASIAN 1996. 321--332.

Digital Library

[21]

X. Li, D. V. Huang, and T. Zheng. 1997. Checking hybrid automata for linear duration invariants. In ASIAN 1997. 166--180.

Digital Library

[22]

J. Liu. 2000. Real-Time Systems. Prentice Hall.

[23]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. 2008. Model checking Duration Calculus: a practical approach. Formal Aspects of Computing 20, 4 (2008), 481--505.

[24]

P. K. Pandya. 2001. Specifying and deciding quantified discrete-time duration calculus formulae using DCVALID. In RT-TOOLS 2001.

[25]

W. L. Pearn, S. H. Chung, A. Y. Chen, and M. H. Yang. 2004. A case study on the multistage IC final testing scheduling problem with reentry. International J. of Production Economics 88, 3 (2004), 257 - 267.

[26]

P. Pettersson. 1999. Modelling and Verification of Real-Time Systems Using Timed Automata: Theory and Practice. PhD thesis. Uppsala University.

[27]

T. G. Rokicki. 1993. Representing and Modeling Digital Circuits. PhD thesis. Stanford University.

Digital Library

[28]

B. Sharma, P. K. Pandya, and S. Chakraborty. 2005. Bounded validity checking of interval duration logic. In TACAS 2005. 301--316.

Digital Library

[29]

A. Tarski. 1951. A Decision Method for Elementary Algebra and Geometry. University of California Press, Berkeley.

[30]

P. Thai and D. Hung. 2004. Verifying linear duration constraints of timed automata. In ICTAC 2004. 295--309.

Digital Library

[31]

M. Zhang, D. Hung, and Z. Liu. 2008. Verification of LDIs by model checking CTL properties. In ICTAC 2008. 395--409.

Digital Library

[32]

M. Zhang, Z. Liu, and N. Zhan. 2009. Model checking linear duration invariants of networks of automata. In FSEN 2009. 244--259.

Digital Library

[33]

C. Zhou and M. R. Hansen. 2004. Duration Calculus: A Formal Approach to Real-Time Systems. Springer.

Digital Library

[34]

C. Zhou, M. R. Hansen, and P. Sestoft. 1993. Decidability and undecidability results for duration calculus. In STACS 1993. 58--68.

Digital Library

[35]

C. Zhou, J. Zhang, L. Yang, and X. Li. 1994. Linear duration invariants. In FTRTFT 1994. 86--109.

Digital Library

[36]

Q. Zu, M. Zhang, J. Zhu, and N. Zhan. 2013. Bounded model-checking of discrete duration calculus. In HSCC 2013. 213--222.

Digital Library

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Kosiuczenko P(2023)Temporal Analysis and Classification of Sensor SignalsSensors10.3390/s2306301723:6(3017)Online publication date: 10-Mar-2023
https://doi.org/10.3390/s23063017
Kosiuczenko P(2021)An Interval Temporal Logic for Time Series Specification and Data IntegrationRemote Sensing10.3390/rs1312223613:12(2236)Online publication date: 8-Jun-2021
https://doi.org/10.3390/rs13122236
Show More Cited By

Index Terms

Model Checking Bounded Continuous-time Extended Linear Duration Invariants
1. Software and its engineering
  1. Software notations and tools
    1. System description languages
      1. System modeling languages
2. Theory of computation
  1. Logic
    1. Verification by model checking
  2. Models of computation
    1. Timed and hybrid models

Recommendations

Bounded model-checking of discrete duration calculus
HSCC '13: Proceedings of the 16th international conference on Hybrid systems: computation and control

Fraenzle and Hansen investigated the model-checking problem of the subset of Duration Calculus without individual variables and quantifications w.r.t. some approximation semantics by reduction to the decision problem of Presburger Arithmetic, thus ...
A practical approach to model checking Duration Calculus using Presburger Arithmetic

This paper investigates the feasibility of reducing a model-checking problem K ⊧ ϕ for discrete time Duration Calculus to the decision problem for Presburger Arithmetic. Theoretical results point at severe limitations of this approach: (1) the ...
Comparing model checking and logical reasoning for real-time systems
Abstract.
We apply both model checking and logical reasoning to a real-time protocol for mutual exclusion. To this end we employ PLC-Automata, an abstract notion of programs for real-time systems. A logic-based semantics in terms of Duration Calculus is ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

HSCC '18: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)

April 2018

296 pages

ISBN:9781450356428

DOI:10.1145/3178126

Copyright © 2018 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 11 April 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

HSCC '18

Sponsor:

SIGBED

HSCC '18: 21st International Conference on Hybrid Systems: Computation and Control

April 11 - 13, 2018

Porto, Portugal

Acceptance Rates

Overall Acceptance Rate 153 of 373 submissions, 41%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
147
Total Downloads

Downloads (Last 12 months)6
Downloads (Last 6 weeks)1

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Fatnassi WShoukry Y(2024)PolyARBerNN: A Neural Network Guided Solver and Optimizer for Bounded Polynomial InequalitiesACM Transactions on Embedded Computing Systems10.1145/363297023:2(1-26)Online publication date: 24-Jan-2024
https://dl.acm.org/doi/10.1145/3632970
Kosiuczenko P(2023)Temporal Analysis and Classification of Sensor SignalsSensors10.3390/s2306301723:6(3017)Online publication date: 10-Mar-2023
https://doi.org/10.3390/s23063017
Kosiuczenko P(2021)An Interval Temporal Logic for Time Series Specification and Data IntegrationRemote Sensing10.3390/rs1312223613:12(2236)Online publication date: 8-Jun-2021
https://doi.org/10.3390/rs13122236
Dole KGupta AKomp JKrishna STrivedi A(2021)Event-Triggered and Time-Triggered Duration Calculus for Model-Free Reinforcement Learning2021 IEEE Real-Time Systems Symposium (RTSS)10.1109/RTSS52674.2021.00031(240-252)Online publication date: Dec-2021
https://doi.org/10.1109/RTSS52674.2021.00031
Rahim MAl-Shaer EDuan Q(2020)A Formal Verification of Configuration-Based Mutation Techniques for Moving Target DefenseSecurity and Privacy in Communication Networks10.1007/978-3-030-63086-7_5(61-79)Online publication date: 12-Dec-2020
https://doi.org/10.1007/978-3-030-63086-7_5

View Options

Login options

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

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten