Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems

  • Conference paper
  • First Online:
Information and Communication Technologies in Education, Research, and Industrial Applications (ICTERI 2014)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 469))

  • 549 Accesses

Abstract

We propose a decidable formal theory which describes high-level properties of abstract continuous-time dynamical systems called Nondeterministic Complete Markovian Systems (NCMS). NCMS is a rather general class of systems which can represent discrete and/or continuous evolutions in continuous time and which is sufficient for modeling a wide range of real-time information processing and cyber-physical systems (CPS). We illustrate the obtained results with a proof of the mutual exclusion property of a CPS which implements Peterson’s algorithm.

This work was supported in part by the research project No. 11BF015-02 “Formal specifications and methods of development of reliable software systems”, Taras Shevchenko National University of Kyiv, Ukraine.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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

Similar content being viewed by others

References

  1. Baheti, R., Gill, H.: Cyber-physical systems. In: Samad, T., Annaswamy, A. (eds.) The Impact of Control Technology, pp. 161–166. IEEE, New York (2011)

    Google Scholar 

  2. Lee, E.A., Seshia, S.A.: Introduction to embedded systems: a cyber-physical systems approach. Lulu.com (2013)

    Google Scholar 

  3. Shi, J., Wan, J., Yan, H., Suo, H.: A survey of cyber-physical systems. In: 2011 International Conference on Wireless Communications and Signal Processing (WCSP), pp. 1–6. IEEE (2011)

    Google Scholar 

  4. Sunder, S.S., et al. (originator): Cyber-physical systems - a concept map. http://cyberphysicalsystems.org/

  5. Barbashin, E.: Introduction to Stability Theory. Nauka (in Russian), Moscow (1967)

    Google Scholar 

  6. Emelyanov, S.: Variable Structure Systems. Nauka (in Russian), Moscow (1967)

    Google Scholar 

  7. Utkin, V.I.: Sliding Modes in Control and Optimization. Communications and Control Engineering. Springer, Heidelberg (1992)

    Book  MATH  Google Scholar 

  8. Samoilenko, A., Perestyuk, N.: Impulsive Differential Equations. World Scientific, Singapore and River Edge (1995)

    MATH  Google Scholar 

  9. Lakshmikantham, V., Banov, D.D., Simeonov, P.S.: Theory of Impulsive Differential Equations. World Scientific Publishing Company, Singapore (1989)

    Book  MATH  Google Scholar 

  10. Filippov, A.: Differential Equations with Discontinuous Righthand Sides: Control Systems. Mathematics and Its Applications. Springer, New York (1988)

    Book  Google Scholar 

  11. Liberzon, D.: Switching in Systems and Control. Systems & Control: Foundations & Applications. Birkhauser Boston Inc., Boston (2003)

    Book  MATH  Google Scholar 

  12. Witsenhausen, H.: A class of hybrid-state continuous-time dynamic systems. IEEE Trans. Autom. Control 11, 161–167 (1966)

    Article  Google Scholar 

  13. Tavernini, L.: Differential automata and their discrete simulators. Nonlinear Anal. Theor. Methods Appl. 11, 665–683 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  14. Nerode, A., Kohn, W.: Models for hybrid systems: automata, topologies, controllability, observability. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 317–356. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  15. Branicky, M.S.: Studies in hybrid systems: modeling, analysis, and control. Ph.D. thesis, Massachusetts Institute of Technology (1995)

    Google Scholar 

  16. Goebel, R., Sanfelice, R.G., Teel, A.: Hybrid dynamical systems. IEEE Control Syst. Mag. 29, 28–93 (2009)

    Article  MathSciNet  Google Scholar 

  17. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  18. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoret. Comput. Sci. 138, 3–34 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  19. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings of Eleventh Annual IEEE Symposium Logic in Computer Science LICS ’96, pp. 278–292 (1996)

    Google Scholar 

  20. Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: de Bakker, J.W., Huizing, C., de Roever, W.P., Rozenberg, G. (eds.) REX 1991. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  21. Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 74–88. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  22. Lynch, N., Segala, R., Vaandrager, F.: Hybrid i/o automata. Inf. Comput. 185, 105–157 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  23. Barringer, H., Kuiper, R., Pnueli, A.: A really abstract concurrent model and its temporal logic. In: POPL, pp. 173–183. ACM Press (1986)

    Google Scholar 

  24. Rabinovich, A.: On the decidability of continuous time specification formalisms. J. Logic Comput. 8, 669–678 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  25. Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Wagner, K.W., Finkel, A. (eds.) STACS 1993. LNCS, vol. 665, pp. 58–68. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  26. Li, X.: Decidability of mean value calculus. J. Comp. Sci. Tech. 14, 173–180 (1999)

    Article  MATH  Google Scholar 

  27. Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)

    Book  Google Scholar 

  28. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20, 309–352 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  29. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reas. 41, 143–189 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  30. Rabinovich, A.: On translations of temporal logic of actions into monadic second order logic. Theoret. Comput. Sci. 193, 197–214 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  31. Bellini, P., Mattolini, R., Nesi, P.: Temporal logics for real-time system specification. ACM Comput. Surv. 32, 12–42 (2000)

    Article  Google Scholar 

  32. Hirshfeld, Y., Rabinovich, A.: Logics for real time: decidability and complexity. Fundam. Inf. 62, 1–28 (2004)

    MATH  MathSciNet  Google Scholar 

  33. Zhang, J., Johansson, K.H., Lygeros, J., Sastry, S.: Zeno hybrid systems. Int. J. Robust Nonlinear Control 11, 435–451 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  34. Birkhoff, G.D.: Dynamical Systems. American Mathematical Society, New York (1927)

    MATH  Google Scholar 

  35. Nemytskii, V., Stepanov, V.: Qualitative Theory of Differential Equations. GITTL (in Russian), Moscow (1949)

    Google Scholar 

  36. Gottschalk, W.H., Hedlund, G.A.: Topological Dynamics. American Mathematical Society Colloquium Publications, New York (1955)

    MATH  Google Scholar 

  37. Roxin, E.: Local definition of generalized control systems. Mich. Math. J. 13, 91–96 (1966)

    Article  MATH  MathSciNet  Google Scholar 

  38. Hájek, O.: Theory of processes, I. Czech. Math. J. 17, 159–199 (1967)

    Google Scholar 

  39. Sell, G.R.: Differential equations without uniqueness and classical topological dynamics. J. Differ. Equ. 14, 42–56 (1973)

    Article  MATH  MathSciNet  Google Scholar 

  40. Kloeden, P.E.: General control systems. In: Coppel, W.A. (ed.) Mathematical Control Theory. Lecture Notes in Mathematics, vol. 680, pp. 119–137. Springer, Heidelberg (1978)

    Chapter  Google Scholar 

  41. Kalman, R.E., Falb, P.L., Arbib, M.A.: Topics in Mathematical System Theory. Pure & Applied Mathematics S. McGraw-Hill Education, New York (1969)

    MATH  Google Scholar 

  42. Mesarovic, M.D., Takahara, Y.: Abstract Systems Theory. Lecture Notes in Control and Information Sciences. Springer, Heidelberg (1989)

    Book  MATH  Google Scholar 

  43. Matrosov, V.M., Anapolskiy, L., Vasilyev, S.: The Method of Comparison in Mathematical Systems Theory. Nauka (in Russian), Novosibirsk (1980)

    Google Scholar 

  44. Willems, J.C.: Paradigms and puzzles in the theory of dynamical systems. IEEE Trans. Autom. Control 36, 259–294 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  45. Bushaw, D.: Dynamical polysystems and optimisation. J. Differ. Equ. 2, 351–356 (1963)

    MathSciNet  Google Scholar 

  46. Movchan, A.: Stability of processes in two metrics. Applied Math. Mech. (in Russian) 24, 988–1001 (1960)

    Google Scholar 

  47. Hájek, O.: Theory of processes, II. Czech. Math. J. 17, 372–398 (1967)

    Google Scholar 

  48. Ivanov, I.: A criterion for existence of global-in-time trajectories of non-deterministic Markovian systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2012. CCIS, vol. 347, pp. 111–130. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  49. Ivanov, I.: On existence of total input-output pairs of abstract time systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds.) ICTERI 2013. CCIS, vol. 412, pp. 308–331. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  50. Ivanov, I.: An abstract block formalism for engineering systems. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G., Zavileysky, M., Kravtsov, H., Kobets, V., Peschanenko, V.S. (eds.) ICTERI. CEUR Workshop Proceedings, vol. 1000, pp. 448–463. CEUR-WS.org (2013)

    Google Scholar 

  51. Rabin, M.: Decidability of second-order theories and automata on infinite trees. Trans. AMS 141, 1–35 (1969)

    MATH  MathSciNet  Google Scholar 

  52. Abraham, U., Ivanov, I., Nikitchenko, M.: Proving behavioral properties of distributed algorithms using their compositional semantics. In: Proceedings of the First International Seminar Specification and Verification of Hybrid Systems, 10–12 October 2011, Taras Shevchenko National University of Kyiv, pp. 9–19 (2011)

    Google Scholar 

  53. Luke, J. (originator): Sorgenfrey topology. Encyclopedia of Mathematics. http://www.encyclopediaofmath.org/index.php?title=Sorgenfrey_topology

Download references

Acknowledgments

We would like to thank Dr. Martin Strecker and Prof. Louis Féraud of Institut de Recherche en Informatique de Toulouse (IRIT), France for the ideas which inspired this work.

Author information

Authors and Affiliations

  1. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Ievgen Ivanov & Mykola Nikitchenko

  2. Paul Sabatier University, Toulouse, France

    Ievgen Ivanov

  3. Ben-Gurion University, Beer-Sheva, Israel

    Uri Abraham

Authors
  1. Ievgen Ivanov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mykola Nikitchenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Uri Abraham
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Ievgen Ivanov .

Editor information

Editors and Affiliations

  1. Zaporizhzhya National University, Zaporizhzhya, Ukraine

    Vadim Ermolayev

  2. Institute of Applied Informatics, Alpen-Adria-Universität Klagenfurt, Klagenfurt, Austria

    Heinrich C. Mayr

  3. Taras Shevchenko National University of Kyiv, Kyiv, Ukraine

    Mykola Nikitchenko

  4. Kherson State University, Kherson, Ukraine

    Aleksander Spivakovsky

  5. V.N. Karazin Kharkiv National University, Kharkov, Ukraine

    Grygoriy Zholtkevych

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Ivanov, I., Nikitchenko, M., Abraham, U. (2014). On a Decidable Formal Theory for Abstract Continuous-Time Dynamical Systems. In: Ermolayev, V., Mayr, H., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds) Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2014. Communications in Computer and Information Science, vol 469. Springer, Cham. https://doi.org/10.1007/978-3-319-13206-8_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-13206-8_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-13205-1

  • Online ISBN: 978-3-319-13206-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation