Understanding deadlock and livelock behaviors in Hybrid Control Systems

This paper introduces a formal definition and a categorization of Deadlock and Livelock behaviors for a general class of deterministic Hybrid Control Systems (HCS), thus extending the classical notion known for (uncontrolled) discrete transition systems. This characterization hinges on three important aspects: (1) the concept of composition (or interconnection) of HCSs; (2) the notion of control-dependent specification, and that of composition of specifications; (3) the dynamical structure of an HCS and its related behaviors. The first notion is introduced in a novel manner, by including aspects from the literature of discrete transition systems, as well as accounting for classical concepts such as that of feedback interconnection of dynamical systems. The second point allows us to formally express general properties that are of interest from a systems and control theory perspective. The third part discriminates between the different and possibly pathological behaviors that are characteristic to HCSs. After commenting on the issues of Deadlock and Livelock prevention and verification, the article concludes with two case studies.