CISPA
Browse
cispa_all_3931.pdf (454.66 kB)

On Specifications and Proofs of Timed Circuits

Download (454.66 kB)
chapter
posted on 2023-11-29, 18:26 authored by Matthias Fuegger, Christoph LenzenChristoph Lenzen, Ulrich Schmid
Given a discrete-state continuous-time reactive system, like a digital circuit, the classical approach is to first model it as a state transition system and then prove its properties. Our contribution advocates a different approach: to directly operate on the input-output behavior of such systems, without identifying states and their transitions in the first place. We discuss the benefits of this approach at hand of some examples, which demonstrate that it nicely integrates with concepts of self-stabilization and fault-tolerance. We also elaborate on some unexpected artefacts of module composition in our framework, and conclude with some open research questions.

History

Preferred Citation

Matthias Fuegger, Christoph Lenzen and Ulrich Schmid. On Specifications and Proofs of Timed Circuits. In: Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday. 2022.

Primary Research Area

  • Algorithmic Foundations and Cryptography

Legacy Posted Date

2023-04-28

Book Title

Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday

Page Range

107-130

Publisher

Springer Cham

Open Access Type

  • Green

BibTeX

@incollection{cispa_all_3931, title = "On Specifications and Proofs of Timed Circuits", author = "Fuegger, Matthias and Lenzen, Christoph and Schmid, Ulrich", booktitle="{Principles of Systems Design: Essays Dedicated to Thomas A. Henzinger on the Occasion of His 60th Birthday}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC