Causality analysis of synchronous programs with refined clocks

Synchronous languages are based on the synchronous abstraction of time, which divides the execution of programs into an infinite sequence of macro steps that consist of finitely many micro steps. A well-studied problem of this model of computation are cyclic dependencies of micro steps whose constructiveness has to be checked by a causality analysis during compilation. Recently, we showed that temporal refinement can be introduced to imperative synchronous languages by refined clocks. In this paper, we formally define the causality analysis for this extension. To this end, we translate the program into a transition system, which can then be used to verify the correct causal behavior with a model checker. We also list optimizations that can be used by compilers to conservatively approximate causality checking.