Skip to main content
SpringerLink
Log in

Discounted Duration Calculus

  • Conference paper
  • First Online:
FM 2016: Formal Methods (FM 2016)

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

Included in the following conference series:

  • 1368 Accesses

Abstract

To formally reason about the temporal quality of systems discounting was introduced to CTL and LTL. However, these logic are discrete and they cannot express duration properties. In this work we introduce discounting for a variant of Duration Calculus. We prove decidability of model checking for a useful fragment of discounted Duration Calculus formulas on timed automata under mild assumptions. Further, we provide an extensive example to show the usefulness of the fragment.

An early version of this work was presented at the Nordic Workshop of Programming Theory 2015.

H. Ody—This Work is supported by the Deutsche Forschungsgemeinschaft (DFG) within the Research Training Group DFG GRK 1765 SCARE.

M. Fränzle—This Work was partially supported by Deutsche Forschungsgemeinschaft within the Transregional Collaborative Research Center SFB/TR 14 AVACS.

M.R. Hansen—This Work was partially supported by the Danish Research Foundation for Basic Research within the IDEA4CPS project.

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 EPUB and 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

Notes

  1. 1.

    We computed the initial states with Uppaal Tiga [8] by computing a winning strategy for the property \( control : A[]\, true \) with the options -c -w 2 -n 2.

References

  1. Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 424–439. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54862-8_37

    Chapter  Google Scholar 

  2. Alur, R., Dill, D.L.: A theory of timed automata. Theoret. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Symposium on System Structure and Control, pp. 469–474 (1998)

    Google Scholar 

  4. Badban, B., Lange, M.: Exact incremental analysis of timed automata with an SMT-Solver. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS 2011. LNCS, vol. 6919, pp. 177–192. Springer, Heidelberg (2011). doi:10.1007/978-3-642-24310-3_13

    Chapter  Google Scholar 

  5. Bengtsson, J., Yi, W.: On clock difference constraints and termination in reachability analysis of timed automata. In: Dong, J.S., Woodcock, J. (eds.) ICFEM 2003. LNCS, vol. 2885, pp. 491–503. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39893-6_28

    Chapter  Google Scholar 

  6. Bjørner, N., Phan, A.-D., Fleckenstein, L.: \(\nu Z\) - an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_14

    Google Scholar 

  7. Bouyer, P., Larsen, K.G., Markey, N.: Model-checking one-clock priced timed automata. In: Seidl, H. (ed.) FoSSaCS 2007. LNCS, vol. 4423, pp. 108–122. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71389-0_9

    Chapter  Google Scholar 

  8. Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005). doi:10.1007/11539452_9

    Chapter  Google Scholar 

  9. Chaochen, Z., Hansen, M.R.: An adequate first order interval logic. In: Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 584–608. Springer, Heidelberg (1998). doi:10.1007/3-540-49213-5_23

    Chapter  Google Scholar 

  10. Chaochen, Z., Hansen, M.R.: Duration Calculus - A Formal Approach to Real-Time Systems. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004)

    MATH  Google Scholar 

  11. Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993). doi:10.1007/3-540-56503-5_8

    Chapter  Google Scholar 

  12. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  13. de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: Model checking discounted temporal properties. Theoret. Comput. Sci. 345(1), 139–170 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  14. de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003). doi:10.1007/3-540-45061-0_79

    Chapter  Google Scholar 

  15. Fränzle, M.: Model-checking dense-time duration calculus. Formal Aspects Comput. 16(2), 121–139 (2004)

    Article  MATH  Google Scholar 

  16. Fränzle, M., Hansen, M.R.: A robust interpretation of duration calculus. In: Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol. 3722, pp. 257–271. Springer, Heidelberg (2005). doi:10.1007/11560647_17

    Chapter  Google Scholar 

  17. Fränzle, M., Hansen, M.R.: Deciding an interval logic with accumulated durations. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 201–215. Springer, Heidelberg (2007). doi:10.1007/978-3-540-71209-1_17

    Chapter  Google Scholar 

  18. Gottwald, S.: Many-valued logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. The Metaphysics Research Lab of Stanford University (2015). http://plato.stanford.edu/archives/spr2015/entries/logic-manyvalued/

  19. Larsen, K.G., Rasmussen, J.I.: Optimal reachability for multi-priced timed automata. Theoret. Comput. Sci. 390(2–3), 197–213 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  20. Mandrali, E.: Weighted LTL with discounting. In: Moreira, N., Reis, R. (eds.) CIAA 2012. LNCS, vol. 7381, pp. 353–360. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31606-7_32

    Chapter  Google Scholar 

  21. Mandrali, E., Rahonis, G.: On weighted first-order logics with discounting. Acta Informatica 51(2), 61–106 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  22. Meyer, R., Faber, J., Hoenicke, J., Rybalchenko, A.: Model checking duration calculus: a practical approach. Formal Aspects Comput. 20(4–5), 481–505 (2008)

    Article  MATH  Google Scholar 

  23. Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006). doi:10.1007/11814948_18

    Chapter  Google Scholar 

  24. Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng. 19(1), 41–55 (1993)

    Article  Google Scholar 

  25. Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds.) Foundations of Information Technology in the Era of Network and Mobile Computing. ITIFIP, vol. 96, pp. 485–497. Springer, Heidelberg (2002). doi:10.1007/978-0-387-35608-2_40

    Chapter  Google Scholar 

Download references

Acknowledgement

We thank Peter Gjøl Jensen for advice on how to compute the set of reachable zones with UPPAAL TIGA.

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Oldenburg, Oldenburg, Germany

    Heinrich Ody & Martin Fränzle

  2. DTU Compute, Technical University of Denmark, Kongens Lyngby, Denmark

    Michael R. Hansen

Authors
  1. Heinrich Ody
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Fränzle
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael R. Hansen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Heinrich Ody .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    John Fitzgerald

  2. US Naval Research Laboratory, Washington, District of Columbia, USA

    Constance Heitmeyer

  3. ISTI-CNR, Pisa, Italy

    Stefania Gnesi

  4. University of Cyprus, Nicosia, Cyprus

    Anna Philippou

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Ody, H., Fränzle, M., Hansen, M.R. (2016). Discounted Duration Calculus. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds) FM 2016: Formal Methods. FM 2016. Lecture Notes in Computer Science(), vol 9995. Springer, Cham. https://doi.org/10.1007/978-3-319-48989-6_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48989-6_35

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48988-9

  • Online ISBN: 978-3-319-48989-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation