On discretization of delays in timed automata and digital circuits.

*(English)*Zbl 0933.94045
Sangiorgi, Davide (ed.) et al., CONCUR ’98. Concurrency theory. 9th international conference, Nice, France, September 8–11, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1466, 470-484 (1998).

Summary: The authors solve the following problem: “given a digital circuit composed of gates whose real-valued delays are in an integer-bounded interval, is there a way to discretize time while preserving the qualitative behavior of the circuit?” This problem is described as open in J. A. Brzozowski and C.-J. H. Seger [Asynchronous circuits, Springer (1994)]. When “preservation of qualitative behavior” is interpreted in a strict sense, as having all original sequences of events with their original ordering they obtain the following two results: 1) For acyclic (combinatorial) circuits whose inputs change only once, the answer is positive: there is a constant \(\delta\), depending on the maximal number of possible events in the circuit, such that if they restrict all events to take place at multiples of \(\delta\), they still preserve qualitative behaviors.

2) For cyclic circuits the answer is negative: a simple circuit with three gates can demonstrate a qualitative behavior which cannot be captured by any discretization.

Nevertheless the authors show that a weaker notion of preservation, similar to that of T. Henzinger, Z. Manna and A. Pnueli [What good are digital clocks?, in W. Kuich (ed.), Proc. ICALP’92, Lect. Notes Comput. Sci. 623, 545-558 (1992)], allows in many cases to verify discretized circuits with \(\delta=1\) such that the verification results are valid in dense time.

For the entire collection see [Zbl 0895.00051].

2) For cyclic circuits the answer is negative: a simple circuit with three gates can demonstrate a qualitative behavior which cannot be captured by any discretization.

Nevertheless the authors show that a weaker notion of preservation, similar to that of T. Henzinger, Z. Manna and A. Pnueli [What good are digital clocks?, in W. Kuich (ed.), Proc. ICALP’92, Lect. Notes Comput. Sci. 623, 545-558 (1992)], allows in many cases to verify discretized circuits with \(\delta=1\) such that the verification results are valid in dense time.

For the entire collection see [Zbl 0895.00051].

##### MSC:

94C10 | Switching theory, application of Boolean algebra; Boolean functions (MSC2010) |