A Complete Proof System for Timed Observations

Y. Ortega Mallen, D. de Frutos Escrig

	   Timed Observations is a failure and divergence semantic
	   model for concurrent processes, suitable for real-time
	   systems. Actions are not instantaneous but need some time to
	   complete their execution, and `true' concurrency is expressed
	   by action multisets (bags). Time is global and discrete.
	   The model is applied to TCSP, obtaining a denotational
	   semantics, for which a complete proof system is developed.