JAIST Logic@JAIST

LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps

  • Eugenio Moggi
  • University of Genova
Date: 2016/08/04 (Thu) 13:30 to 15:10
Place: JAIST, Collaboration room 7 (I-56)
Group: Logic Unit, Core2Core

Hybrid systems (HS) are dynamic systems that exhibit both continuous and discrete dynamic behavior: they can flow (according to a differential equation) and jump (according to a transition relation). HS can be used for modeling rigid body dynamics with impacts, and more generally Cyber-Physical Systems. HS can exhibit Zeno behaviors, that arise naturally in rigid body dynamics with impacts, but are absent from purely discrete or purely continuous systems. Dealing properly with these behaviors is a prerequisite to give sound definitions of concepts such as reachability. We propose the use of partial continuous maps (PCM) as trajectories that describe how a HS evolves over time. PCMs enable a notion of trajectory that can go beyond Zeno points.