Operational semantics for timed systems

Viac o knihe

This monograph introduces a novel approach for uniform modeling of timed and hybrid systems. Heinrich Rust presents a time model that accommodates both discrete time steps and continuous processes through a dense real-number time framework. This model effectively expresses event synchronicity in a real-number context while maintaining strict causality using uniform discrete time steps. By integrating these two commonly separated views of time, it addresses the modeling challenges in discrete systems, where time is represented by uniform discrete steps, and continuous systems, which perceive time as a dense flow. The key innovation lies in discretizing the dense real-number time structure using constant infinitesimal time steps at each real-number point. The mathematical foundation of this model draws on Non-standard Analysis concepts introduced by Abraham Robinson in the 1950s. Discrete modeling is achieved through Abstract State Machines, utilizing the formalisms developed by Yuri Gurevich and temporal logic. Together, these elements create a robust formal basis for describing a wide range of systems with quantitative linear time properties, facilitating the seamless integration, refinement, and embedding of continuous and discrete models into a cohesive framework known as "Non-standard Timed Abstract State Machines" (NTASM).