Translating synchronous guarded actions to interleaved guarded actions

In general, guarded actions are well suited to describe systems with different models of computations (MoCs). Different MoCs are thereby obtained by different ways to select actions for execution: In particular, in synchronous models, one executes all enabled actions, in interleaved models, one executes one of the enabled actions, and in asynchronous models, some non-empty subset of the enabled actions is executed. It seems to be impossible to use tools for one of these MoCs for guarded actions that are based on another MoC. In particular, it is unfortunate for the synchronous models that many rewrite-based verification tools and theorem provers are based on interleaved MoCs. In this paper, we therefore develop a translation from synchronous guarded actions (SGAs) to interleaved guarded actions (IGAs). This allows us to use many established tools for formal verification also for systems represented by SGAs. To achieve this, we have to solve four major problems: first, the causal execution order of the synchronous guarded actions must be encoded in the IGAs. Second, the different behaviors of immediate and delayed assignments of our SGAs must be preserved. Third, it must be guaranteed that all IGAs of one macro step are executed before the IGAs of the next macro step are started. Finally, temporal logic specifications stated for the SGAs have to be adequately adapted for IGAs. Our results are finally used to verify SGAs obtained by compilation of synchronous programs by means of the symbolic analysis laboratory (SAL) of SRI.