Detectability of Nondeterministic Finite-Transition Systems
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.
- Baier C, Katoen JP (2008) Principles of model checking. The MIT PressGoogle Scholar
- Belta C, Yordanov B, Gol EA (2017) Formal methods for discrete-time dynamical systems. Springer International Publishing AGGoogle Scholar
- Kari J (2016) Cellular automata. http://users.utu.fi/jkari/ca2016/
- Tabuada P (2009) Verification and control of hybrid systems: a symbolic approach, 1st edn. Springer Publishing CompanyGoogle Scholar
- Zhang K, Yin X, Zamani M (2018) Opacity of nondeterministic transition systems: a (bi)simulation relation approach. IEEE Trans Autom Control. https://arxiv.org/abs/1802.03321
- Zhang K, Zamani M (2017) Detectability of nondeterministic finite transition systems. In: IFAC PapersOnline, vol 50-1, pp 9272–9277Google Scholar