Reachability analysis of dynamical systems having piecewise-constant derivatives. (English) Zbl 0884.68050

Asarin, Eugene; Maler, Oded; Pnueli, Amir

Theor. Comput. Sci. 138, No. 1, 35-65 (1995).

Summary: We consider a class of hybrid systems, namely dynamical systems with piecewise-constant derivatives (PCD systems). Such systems consist of a partition of the Euclidean space into a finite set of polyhedral sets (regions). Within each region the dynamics is defined by a constant vector field, hence discrete transitions occur only on the boundaries between regions where the trajectories change their direction.
With respect to such systems we investigate the reachability question: Given an effective description of the systems and of two polyhedral subsets \(P\) and \(Q\) of the state-space, is there a trajectory starting at some \(x\in P\) and reaching some point in \(Q\)? Our main results are a decision procedure for two-dimensional systems, and an undecidability result for three or more dimensions.

MSC:

68Q10	Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
93B05	Controllability

Keywords:

PCD systems; dynamical systems; piecewise-constant derivatives; reachability

References:

[1]	Alur, R.; Courcoubetis, C.; Dill, D. L., Model checking in dense real time, Inform. and Comput., 104, 2-34 (1993) · Zbl 0783.68076
[2]	Alur, R.; Courcoubetis, C.; Henzinger, T.; Ho, P., Hybrid automata: an algorithmic appraoch to the specification and analysis of hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 209-229
[3]	Alur, R.; Dill, D. L., A theory of time automata, Theoret. Comput. Sci., 126, 183-235 (1994) · Zbl 0803.68071
[4]	Asarin, A.; Maler, O., On some relations between dynamical systems and transition systems, (Abiteboul, S.; Shamir, E., Proc ICALP ’94. Proc ICALP ’94, Lecture Notes in Computer Science, Vol. 820 (1994), Springer: Springer Berlin), 59-72 · Zbl 1418.68088
[5]	Branicky, M. S., Universal computation and other capabilities of hybrid and continuous dynamical systems, Theoret. Comput. Sci., 138, 67-100 (1995), this issue · Zbl 0874.68207
[6]	Brockett, R. W., Smooth dynamical systems which realize arithmetical and logical operations, (Nijmeijer, H.; Schumacher, J. M., Three Decades of Mathematical Systems Theory. Three Decades of Mathematical Systems Theory, Lecture Notes in Control and Information Sciences (1989), Springer: Springer Berlin), 19-30 · Zbl 0683.93049
[7]	Brondsted, A., An Introduction to Convex Polytopes (1983), Springer: Springer New York · Zbl 0509.52001
[8]	Cosnard, M.; Garzon, M.; Koiran, P., Computability properties of low-dimensional dynamical systems, (Enjalbert, P.; Finkel, A.; Wagner, K. W., Proc. 10th Ann. Symp. on Theoretical Aspects of Computer Science. Proc. 10th Ann. Symp. on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science, Vol. 665 (1993), Springer: Springer Berlin), 365-373 · Zbl 0791.68056
[9]	DeMillo, R. A.; Lipton, R. J., Defining software by continuous smooth functions, IEEE Trans. Software Eng., 17, 383-384 (1991)
[10]	Henzinger, T.; Nicollin, X.; Sifakis, J.; Yovine, S., Symbolic model-checking for real-time systems, Inform. and Comput., 111, 193-244 (1994) · Zbl 0806.68080
[11]	Hopcroft, J. E.; Ullman, J. D., Introduction to Automata Theory, Languages and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0196.01701
[12]	Kesten, Y.; Pnueli, A.; Sifakis, J.; Yovine, S., Integration graphs: a class of decidable hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 179-208
[13]	Maler, O.; Manna, Z.; Pnueli, A., From timed to hybrid systems, (de Bakker, J. W.; Huizing, C.; de Roever, W. P.; Rozenberg, G., Proc. REX Workshop Real Time: Theory in Practice. Proc. REX Workshop Real Time: Theory in Practice, Lecture Notes in Computer Science, Vol. 600 (1992), Springer: Springer Berlin), 447-484
[14]	Maler, O.; Pnueli, A., Reachability analysis of planar multi-linear systems, (Courcoubetis, C., Proc. 5th Work-shop on Computer-Aided Verification. Proc. 5th Work-shop on Computer-Aided Verification, Lecture Notes in Computer Science, Vol. 697 (1993), Springer: Springer Berlin), 194-209
[15]	Nicollin, X.; Olivero, A.; Sifakis, J.; Yovine, S., An approach to the description and analysis of hybrid systems, (Grossman, R. L.; Nerode, A.; Ravn, A.; Rischel, H., Hybrid Systems. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736 (1993), Springer: Springer Berlin), 149-178
[16]	Putnam, H., Representation and Reality, ((1988), MIT Press: MIT Press Cambridge, MA), 121-125
[17]	Reif, J. H.; Tygar, J. D.; Yoshida, A., The computability and complexity of optical beam tracing, (Proc. 31st Ann. Symp. on Foundations of Computer Science. Proc. 31st Ann. Symp. on Foundations of Computer Science, St. Louis, MO (1990), IEEE Press: IEEE Press New York), 106-114 · Zbl 0807.68096