Paulo Tabuada's selected and annotated bibliography

From Nonlinear to Hamiltonian via Feedback

Paulo Tabuada and George J. Pappas.

IEEE Transactions on Automatic Control, 48(8), 1439-1442, August 2003.

This was my first published journal paper. It addresses the question: which control systems can be rendered Hamiltonian by suitably designing a feedback control law? The answer can be given, locally, by a simple differential geometric condition relating the control system to a chosen symplectic form. A generalization of the results in this paper was later given by Cheng, Astolfi, and Ortega in the paper On feedback equivalence to port controlled Hamiltonian systems.

This question was motivated and partially addresses the problem posed by Block, Leonard, and Marsden in the book Open Problems in Mathematical Systems and Control Theory.

Bisimilar Control Affine Systems

Paulo Tabuada and George J. Pappas.

Systems and Control Letters, 52(1), 49-58, May 2004.

The notion of Bisimulation was brought by George J. Pappas from Computer Science to Control Theory in the paper Bisimilar linear systems. As can be inferred from the title, only linear control systems were considered. The nonlinear case, for input affine systems, was studied in Bisimilar Control Affine Systems using differential geometric techniques. It was shown that bisimilarity can be characterized using the notion of controlled invariant distribution that appeared some 20 years before in the context of differential geometric control theory. Similar results were independently developed by Arjan van der Schaft and appeared in the paper Equivalence of Dynamical Systems by Bisimulation.

Linear Time Logic control of discrete-time linear systems

Paulo Tabuada and George J. Pappas

IEEE Transactions on Automatic Control, 51(12), 1862-1877, December 2006

Linear Time Logic (LTL) or Linear Temporal Logic is a logic frequently used in the specification and verification of temporal properties of software. The LTL verification problem asks if, given a LTL formula f and a program P, all the executions of P satisfy the formula f. In this paper we solved the LTL synthesis problem for discrete-time linear control systems. The LTL synthesis problem asks if, given a LTL formula f and a control system S, there exists a controller C forcing the closed-loop system C||S to satisfy the formula f. The solution is based on a general result stating that controllable linear systems in discrete-time with suitably defined outputs are equivalent, in the bisimulation sense, to finite-state machines. A more general version of this result appears in the book Verification and Control of Hybrid Systems where it is shown that controllability can be dropped by suitably restricting the outputs. This paper identified the first broad class of control systems known to be equivalent to finite-state machines: discrete-time linear systems. A preliminary version of these results appeared in Model Checking LTL over Controllable Linear Systems Is Decidable.

Event-triggered real-time scheduling of stabilizing control tasks

Paulo Tabuada

IEEE Transactions on Automatic Control, 52(9), 1680-1685, September 2007.

I wrote this paper to bring to fruition an alternative paradigm for the real-time scheduling of control tasks. Traditionally, control tasks have been treated as periodic hard-real time tasks. Several researchers, including Karl-Erik Arzen in the paper A simple event-based PID controller, and Astrom and Bernhardsson in the paper Comparison of Riemann and Lebesgue sampling for first order stochastic systems, had exposed the advantages of modeling control tasks as event-triggered rather than time-triggered (and periodic). However, a concrete design methodology for event-triggered implementations was lacking. In this paper I showed how a simple event-triggering rule can be designed for the sample-and-hold implementation of stabilizing control laws. The event-triggered implementation exploits the robustness properties of the control law to drastically reduce the processor time devoted to control while guaranteeing desired levels of performance. A preliminary version of these results appeared in Preliminary results on state-trigered scheduling of stabilizing control tasks.

Controller synthesis for bisimulation equivalence

Paulo Tabuada

Systems and Control Letters, 57(6), 443-452, June 2008.

This paper arose while trying to distill the proof techniques in Branching time controllers for discrete event systems. It became apparent that the conditions for the existence of a controller enforcing bisimulation equivalence could be stated directly by requiring the existence of a certain alternating simulation relation. Moreover, such statement could be interpreted in a wide range of settings including transition systems, probabilistic transition systems, timed transition systems, Petri nets, control systems, and so on. It was also clear that the natural language to make and prove such statements in fairly general way was Category Theory. Since the publication of a preliminary conference version (Open Maps, Alternating Simulations and Control Synthesis), the results have generalized, by eliminating a certain observability assumption, in the specific context of automata (Control of nondeterministic discrete-event systems for bisimulation equivalence) and linear control systems (On achievable bisimulations for linear time-invariant systems).

Approximately bisimilar symbolic models for nonlinear control systems

Giordano Pola, Antoine Girard and Paulo Tabuada

Automatica, 44(10), 2508-2516, October 2008.

The equivalence between finite automata and discrete-time linear control systems described in the paper Linear Time Logic control of discrete-time linear systems established a bridge between the models used in control theory and the models used in formal methods. After several attempts to extend these results to continuous-time systems, Giordano Pola, Antoine Girard, and myself were able to identify two key ingredients enabling a similar equivalence in continuous-time: the notion of approximate bisimulation, and the notion of incremental input-to-state stability. Approximate bisimulation was introduced axiomatically in control theory by Antoine Girard and George J. Pappas in the paper Approximation metrics for discrete and continuous systems and was introduced constructively using set-valued output maps in the paper An Approximate Simulation Approach to Symbolic Control. Incremental stability is an old concept that was studied recently under the modern input-to-state stability perspective by David Angeli in the paper A Lyapunov approach to incremental stability properties. These two ingredients can be combined to show that any incrementally input-to-state stable nonlinear control system with compact state-space is approximately bisimilar to a finite automaton.