Detectability of Nondeterministic Finite-Transition Systems

  • Kuize ZhangEmail author
  • Lijun Zhang
  • Lihua Xie
Part of the Communications and Control Engineering book series (CCE)


In the past few years, important applications of nondeterministic finite-transition systems (NFTSs) in formal verification and synthesis of (infinite-state) continuous (or hybrid) control systems have been witnessed (Tabuada 2009; Belta et al. 2017; Kloetzer and Belta 2008; Reissig 2011; Zamani 2014; Girard and Pappas 2007). In this methodology, the requirements or specifications for the control systems are described using temporal logics or automata Baier and Katoen (2008). Then, one constructs finite and often nondeterministic abstractions (NFTSs) of the control systems with the property that discrete (or symbolic) controllers designed on the abstractions by using automata-theoretic algorithms from computer science can be refined into controllers on the original control systems to make the requirements be met.


  1. Baier C, Katoen JP (2008) Principles of model checking. The MIT PressGoogle Scholar
  2. Belta C, Yordanov B, Gol EA (2017) Formal methods for discrete-time dynamical systems. Springer International Publishing AGGoogle Scholar
  3. Girard A, Pappas GJ (2007) Approximation metrics for discrete and continuous systems. IEEE Trans Autom Control 52(5):782–798MathSciNetCrossRefGoogle Scholar
  4. Kari J (2016) Cellular automata.
  5. Kloetzer M, Belta C (2008) A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans Autom Control 53(1):287–297MathSciNetCrossRefGoogle Scholar
  6. Reissig G (2011) Computing abstractions of nonlinear systems. IEEE Trans Autom Control 56(11):2583–2598MathSciNetCrossRefGoogle Scholar
  7. Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach, 1st edn. Springer Publishing CompanyGoogle Scholar
  8. Zamani M et al (2014) Symbolic control of stochastic systems via approximately bisimilar finite abstractions. IEEE Trans Autom Control 59(12):3135–3150MathSciNetCrossRefGoogle Scholar
  9. Zhang K, Yin X, Zamani M (2018) Opacity of nondeterministic transition systems: a (bi)simulation relation approach. IEEE Trans Autom Control.
  10. Zhang K, Zamani M (2017) Detectability of nondeterministic finite transition systems. In: IFAC PapersOnline, vol 50-1, pp 9272–9277Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.School of Electrical Engineering and Computer ScienceKTH Royal Institute of TechnologyStockholmSweden
  2. 2.School of Marine Science and TechnologyNorthwestern Polytechnical UniversityXi’anChina
  3. 3.School of Electrical and Electronic EngineeringNanyang Technological UniversitySingaporeSingapore

Personalised recommendations