Extending Process Languages with Time

摘要

In recent years a large number of process languages with time have been developed as more realistic formalisms for description and reasoning about concurrent systems. We propose a uniform framework, based on the ordered structural operational semantics (SOS) approach, for extending arbitrary process languages with discrete time. The generality of our framework allows the user to select the most suitable timed process language for a tsk in hand. This is possible because the user can choose any operators, whether they are standard or new application-specific operators, provided that they preserve a version of weak bisimulation and all processes in the considered language satisfy the time determininacy property. We also propose several constraints on ordered SOS rules for the operators such that some other properties, which reflect the nature of time passage, are satisfied.