Rule Formats for Timed Processes

Building on previous work [15,8], this paper describes two syntactic ways of defining `well-behaved' operational semantics for timed processes. In both cases, the rules are derived from abstract operational rules for behaviour comonads and thus ensure congruence results. The first of them, a light-weight attempt usmatic rules, is shown to be sound, i.e., to indeed induce abstract rules as introduced in [8]. Then a second format, based on a new and very general kind of rules, comonadic SOS (CSOS), is presented which uses meta rules and is also complete, i.e., it characterises all possible CSOS rules for timed processes.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Marco Kick
• Keywords: Abstract Operational Rules, Attempt Usmatic Rules, ENTCS 2002, Syntactic Ways