A Decidable Clock Language for Synchronous Specifications

Abstract:
Presence and absence of signals inside a reaction are inherent to the synchronous paradigm. Clocks are sets of instants (indicating for example when a signal is present) mainly used to describe the control part of data-flow specifications. The language CL we define here expresses relations between clocks. Such relations can describe the combinational part of specifications, as well as particular instantaneous safety properties. We give a decision procedure for CL and apply it to the model-checking of Signal programs abstracted from their state handling part. Thanks to the use of clocks, absence is not explicitly encoded by a special value.

Bibtex entry:

@InProceedings{nebutpinchinat-slap02,
  author = 	 {M. Nebut and S. Pinchinat},
  title = 	 {A Decidable Clock Language for Synchronous Specifications},
  booktitle = 	 {Synchronous Languages, Applications, and Programming},
  key =		 {SLAP'02},
  year =	 2002,
  volume =	 65,
  number =	 5,
  address =	 {Grenoble, France},
  month =	 {april},
  publisher =	 {Electronic Notes in Theoretical Computer Science}
}

files (PS,PDF)

Mirabelle Nebut

Last modified: Fri Jun 10 15:09:49 CEST 2005