Skip to main content
SpringerLink
Log in

Monitoring Realizability

  • Conference paper
Runtime Verification (RV 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7186))

Included in the following conference series:

Abstract

We present a new multi-valued monitoring approach for linear-time temporal logic that classifies trace prefixes not only according to the existence of correct and erroneous continuations, but also according to the strategic power of the system and its environment to avoid or enforce a violation of the specification. We classify the monitoring status into four levels: (1) the worst case is a violation, where no continuation satisfies the specification any more; (2) unrealizable means that the environment can force the system to violate the specification; (3) realizable means that the system can enforce that the specification is satisfied; (4) the best case, fulfilled, indicates that all possible continuations satisfy the specification. Because our approach recognizes situations where the system cannot avoid a violation even though there may still be continuations in which the specification is satisfied, our approach detects errors earlier, and it detects errors that are missed by less detailed classifications. We give an asymptotically optimal construction of multi-valued monitoring automata based on parity games.

This work was partly supported by the German Research Foundation (DFG) under the project SpAGAT (grant no. FI 936/2-1) in the priority programme “Reliably Secure Software Systems – RS3”.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bauer, A., Leucker, M., Schallhart, C.: Runtime verification for LTL and TLTL. ACM Transactions on Software Engineering and Methodology 20(4) (2011)

    Google Scholar 

  2. Büchi, J., Landweber, L.: Solving sequential conditions by finite-state strategies. Trans. AMS (138) (1969)

    Google Scholar 

  3. D’Amorim, M., Roşu, G.: Efficient Monitoring of ω-Languages. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 364–378. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Ehlers, R.: Minimising Deterministic Büchi Automata Precisely Using SAT Solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 326–332. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  5. Ehlers, R.: Short Witnesses and Accepting Lassos in ω-Automata. In: Dediu, A.-H., Fernau, H., Martín-Vide, C. (eds.) LATA 2010. LNCS, vol. 6031, pp. 261–272. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  6. Finkbeiner, B., Kuhtz, L.: Monitor Circuits for LTL with Bounded and Unbounded Future. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 60–75. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  7. Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Formal Methods in System Design 24(2), 101–127 (2004)

    Article  MATH  Google Scholar 

  8. Hopcroft, J.E.: An n log n algorithm for minimizing the states in a finite automaton. In: Kohavi, Z. (ed.) The Theory of Machines and Computations, pp. 189–196. Academic Press (1971)

    Google Scholar 

  9. Jurdziński, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  10. Klein, J., Baier, C.: Experiments with deterministic ω-automata for formulas of linear temporal logic. Theor. Comput. Sci. 363(2), 182–195 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  11. Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291–314 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  12. Küsters, R.: 6 Memoryless Determinacy of Parity Games. In: Grädel, E., Thomas, W., Wilke, T. (eds.) Automata, Logics, and Infinite Games. LNCS, vol. 2500, pp. 95–106. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  13. Müller, S.M., Paul, W.J.: Computer architecture: complexity and correctness. Springer, Heidelberg (2000)

    MATH  Google Scholar 

  14. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57. IEEE (1977)

    Google Scholar 

  15. Pnueli, A., Rosner, R.: On the Synthesis of an Asynchronous Reactive Module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  16. Pnueli, A., Zaks, A., Zuck, L.D.: Monitoring interfaces for faults. Electr. Notes Theor. Comput. Sci. 144(4), 73–89 (2006)

    Article  Google Scholar 

  17. Sentovich, E., Singh, K., Lavagno, L., Moon, C., Murgai, R., Saldanha, A., Savoj, H., Stephan, P., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: SIS: A system for sequential circuit synthesis. Technical Report UCB/ERL M92/41, EECS Department, University of California, Berkeley (1992)

    Google Scholar 

  18. Y., M., Vardi, T.W.: Automata: from logics to algorithms. In: Flum, J., Grädel, E., Wilke, T. (eds.) Logic and Automata: History and Perspectives. Texts in Logic and Games, vol. (2), pp. 629–736. Amsterdam University Press (2007)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Reactive Systems Group, Saarland University, 66123, Saarbrücken, Germany

    Rüdiger Ehlers & Bernd Finkbeiner

Authors
  1. Rüdiger Ehlers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Finkbeiner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Electrical and Computer Engineering, The University of Texas at Austin, 1 University Station C5000, 78712-0240, Austin, TX, USA

    Sarfraz Khurshid

  2. University of California, 581 Soda Hall #1776, 94720-1776, Berkeley, CA, USA

    Koushik Sen

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ehlers, R., Finkbeiner, B. (2012). Monitoring Realizability. In: Khurshid, S., Sen, K. (eds) Runtime Verification. RV 2011. Lecture Notes in Computer Science, vol 7186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-29860-8_34

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-29860-8_34

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-29859-2

  • Online ISBN: 978-3-642-29860-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation