More Web Proxy on the site http://driver.im/

article

Checking Finite Traces Using Alternating Automata

Authors:

Bernd Finkbeiner,

Henny SipmaAuthors Info & Claims

Formal Methods in System Design, Volume 24, Issue 2

Pages 101 - 127

https://doi.org/10.1023/B:FORM.0000017718.28096.48

Published: 01 March 2004 Publication History

Abstract

Alternating automata have been commonly used as a basis for static verification of reactive systems. In this paper we show how alternating automata can be used in runtime verification. We present three algorithms to check at runtime whether a reactive program satisfies a temporal specification, expressed by a linear-time temporal logic formula. The three methods start from the same alternating automaton but traverse the automaton in different ways: depth-first, breadth-first, and backwards, respectively. We then show how an extension of these algorithms, that collects statistical data while verifying the execution trace, can be used for a more detailed analysis of the runtime behavior. All three methods have been implemented and experimental results are presented.

References

[1]

1. N.S. Bjørner, A. Browne, M. Colón, B. Finkbeiner, Z. Manna, H.B. Sipma, and T.E. Uribe, "Verifying temporal properties of reactive systems: A STeP tutorial," Formal Methods in System Design, Vol. 16, No. 3, pp. 227-270, 2000.]]

Digital Library

[2]

2. G. Bruns and P. Godefroid, "Temporal logic query checking," in Proc. 16th IEEE Symp. Logic in Comp. Sci., IEEE Computer Society Press, 2001, pp. 409-417.]]

Digital Library

[3]

3. D. Drusinsky, "The Temporal Rover and the ATG Rover," in K. Havelund, J. Penix, and W. Visser (Eds.), SPIN Model Checking and Software Verification, 7th Int'l SPIN Workshop, Vol. 1885 of LNCS, Springer-Verlag, pp. 323-330, 2000.]]

[4]

4. B. Finkbeiner, S. Sankaranarayanan, and H. B. Sipma, "Collecting statistics over runtime executions," in K. Havelund and G. Rosu (Eds.), Runtime Verification 2002, Vol. 70 of Electronic Notes in Theoretical Computer Science. Elsevier, 2002.]]

[5]

5. K. Havelund, "Using runtime analysis to guide model checking of Java Programs" in K. Havelund, J. Penix, and W. Visser (Eds.), SPIN Model Checking and Software Verification, 7th Int'l SPIN Workshop, Vol. 1885 of LNCS, Springer-Verlag, 2000, pp. 245-264.]]

[6]

6. K. Havelund and G. Rosu, "Testing linear temporal logic formulae on finite execution traces" Technical Report TR 01-08, RIACS, 2001.]]

Digital Library

[7]

7. K. Havelund and G. Rosu (Eds.), "Runtime verification 2001," Vol. 55 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2001.]]

[8]

8. K. Havelund and G. Rosu (Eds.), "Runtime verification 2001" Vol. 70 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2002a.]]

[9]

9. K. Havelund and G. Rosu, "Synthesizing monitors for safety properties;' in Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), Vol. 2280 of LNCS, Springer-Verlag, 2002b, pp. 342-356.]]

Digital Library

[10]

10. M. Kim, S. Kannan, I. Lee, O. Sokolsky, and M. Viswanathan, "Java-MaC: a run-time assurance tool for Java programs," in K. Havelund and G. Rosu (Eds.), Runtime Verification (RV 2001), Vol. 55 of Electronic Notes in Computer Science. Paris, Elsevier Science Publishers, 2001, pp. 115-132.]]

[11]

11. I. Lee, S. Kannan, M. Kim, O. Sokolsky, and M. Viswanathan, "Runtime assurance based on formal specifications;' in Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1999.]]

[12]

12. Z. Manna and A. Pnueli, "Specification and verification of concurrent programs by ∀-automata," in B. Banieqbal, H. Barringer, and A. Pnueli (Eds.), Temporal Logic in Specification, No. 398 in LNCS. Berlin: Springer-Verlag, 1987, pp. 124-164. Also in Proc. 14th ACM Symp. Princ. of Prog. Lang., Munich, Germany, 1987, pp. 1-12.]]

Digital Library

[13]

13. Z. Manna and A. Pnueli, Temporal Verification of Reactive Systems: Safety. New York: Springer-Verlag, 1995.]]

Digital Library

[14]

14. Z. Manna and H.B. Sipma, "Alternating the temporal picture for safety," in U. Montanari, J.D. Rolim, and E. Welzl (Eds.), Proc. 27th Intl. Colloq. Aut. Lang. Prog., Vol. 1853. Geneva, Switzerland, Springer-Verlag, 2000, pp. 429-450.]]

Digital Library

[15]

15. G. Rosu and K. Havelund, "Synthesizing dynamic programming algorithms from linear temporal logic formulae," Technical Report TR 01-15, RIACS, 2001.]]

Digital Library

[16]

16. W. Thomas, "Automata on infinite objects" in J. van Leeuwen (Ed.), Handbook of Theoretical Computer Science, Vol. B. Elsevier Science Publishers North-Holland, 1990, pp. 133-191.]]

Digital Library

[17]

17. M.Y. Vardi, "Alternating automata and program verification," in J. van Leeuwen (Ed.), Computer Science Today. Recent Trends and Developments, Vol. 1000 of LNCS. Springer-Verlag, 1995, pp. 471-485.]]

[18]

18. M.Y. Vardi, "An automata-theoretic approach to linear temporal logic" in F. Moller and G. Birtwistle (Eds.), Logics for Concurrency. Structure versus Automata, Vol. 1043 of LNCS, Springer-Verlag, 1996, pp. 238-266.]]

Digital Library

[19]

19. M.Y. Vardi, "Alternating automata: Checking truth and validity for temporal logics" in Proc. 14th Intl. Conference on Automated Deduction, Vol. 1249 of LNCS. Springer-Verlag, 1997.]]

Digital Library

Cited By

Barrière APit-Claudel C(2024)Linear Matching of JavaScript Regular ExpressionsProceedings of the ACM on Programming Languages10.1145/36564318:PLDI(1336-1360)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656431
Schirmer SSingh JJensen EDauer JFinkbeiner BSankaranarayanan S(2024)Temporal Behavior Trees: Robustness and SegmentationProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650180(1-14)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650180
Mamouras K(2024)Efficient Offline Monitoring for Dynamic Metric Temporal LogicRuntime Verification10.1007/978-3-031-74234-7_8(128-149)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_8
Show More Cited By

Recommendations

Bounded Model Checking with SNF, Alternating Automata, and Büchi Automata

Model checking of LTL formulæis traditionally carried out by a conversion to Büchi automata, and there is therefore a large body of research in this area including some recent studies on the use of alternating automata as an intermediate ...
From LTL to unambiguous Büchi automata via disambiguation of alternating automata
Abstract
Due to the high complexity of translating linear temporal logic (LTL) to deterministic automata, several forms of “restricted” nondeterminism have been considered with the aim of maintaining some of the benefits of deterministic automata, while at ...
Alternating finite automata and related problems

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Formal Methods in System Design

Formal Methods in System Design Volume 24, Issue 2

March 2004

115 pages

ISSN:0925-9856

Issue’s Table of Contents

Copyright © Copyright © 2004 Kluwer Academic Publishers.

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 01 March 2004

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Barrière APit-Claudel C(2024)Linear Matching of JavaScript Regular ExpressionsProceedings of the ACM on Programming Languages10.1145/36564318:PLDI(1336-1360)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656431
Schirmer SSingh JJensen EDauer JFinkbeiner BSankaranarayanan S(2024)Temporal Behavior Trees: Robustness and SegmentationProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650180(1-14)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650180
Mamouras K(2024)Efficient Offline Monitoring for Dynamic Metric Temporal LogicRuntime Verification10.1007/978-3-031-74234-7_8(128-149)Online publication date: 14-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74234-7_8
Basin DKrstić SSchneider JTraytel D(2023)Correct and Efficient Policy Monitoring, a RetrospectiveAutomated Technology for Verification and Analysis10.1007/978-3-031-45329-8_1(3-30)Online publication date: 24-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-45329-8_1
Torfah HXie CJunges SVazquez-Chanlatte MSeshia S(2022)Learning Monitorable Operational Design Domains for Assured AutonomyAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_1(3-22)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_1
Khoury RHallé SLebrun Y(2021)Automata-based monitoring for LTL-FOInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-020-00566-z23:2(137-154)Online publication date: 1-Apr-2021
https://dl.acm.org/doi/10.1007/s10009-020-00566-z
Vargovčík PHolík L(2021)Simplifying Alternating Automata for Emptiness TestingProgramming Languages and Systems10.1007/978-3-030-89051-3_14(243-264)Online publication date: 17-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-89051-3_14
Torfah HJunges SFremont DSeshia S(2021)Formal Analysis of AI-Based Autonomy: From Modeling to Runtime AssuranceRuntime Verification10.1007/978-3-030-88494-9_19(311-330)Online publication date: 11-Oct-2021
https://dl.acm.org/doi/10.1007/978-3-030-88494-9_19
Schwenger M(2020)Monitoring Cyber-Physical Systems: From Design to IntegrationRuntime Verification10.1007/978-3-030-60508-7_5(87-106)Online publication date: 6-Oct-2020
https://dl.acm.org/doi/10.1007/978-3-030-60508-7_5
Keeler CSalomaa K(2020)Alternating Finite Automata with Limited Universal BranchingLanguage and Automata Theory and Applications10.1007/978-3-030-40608-0_13(196-207)Online publication date: 4-Mar-2020
https://dl.acm.org/doi/10.1007/978-3-030-40608-0_13
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents