---
_id: '14735'
abstract:
- lang: eng
  text: "Scaling blockchain protocols to perform on par with the expected needs of
    Web3.0 has been proven to be a challenging task with almost a decade of research.
    In the forefront of the current solution is the idea of separating the execution
    of the updates encoded in a block from the ordering of blocks. In order to achieve
    this, a new class of protocols called rollups has emerged. Rollups have as input
    a total ordering of valid and invalid transactions and as output a new valid state-transition.\r\nIf
    we study rollups from a distributed computing perspective, we uncover that rollups
    take as input the output of a Byzantine Atomic Broadcast (BAB) protocol and convert
    it to a State Machine Replication (SMR) protocol. BAB and SMR, however, are considered
    equivalent as far as distributed computing is concerned and a solution to one
    can easily be retrofitted to solve the other simply by adding/removing an execution
    step before the validation of the input.\r\nThis “easy” step of retrofitting an
    atomic broadcast solution to implement an SMR has, however, been overlooked in
    practice. In this paper, we formalize the problem and show that after BAB is solved,
    traditional impossibility results for consensus no longer apply towards an SMR.
    Leveraging this we propose a distributed execution protocol that allows reduced
    execution and storage cost per executor (O(log2n/n)) without relaxing the network
    assumptions of the underlying BAB protocol and providing censorship-resistance.
    Finally, we propose efficient non-interactive light client constructions that
    leverage our efficient execution protocols and do not require any synchrony assumptions
    or expensive ZK-proofs."
acknowledgement: 'Eleftherios Kokoris-Kogias is partially supported by Austrian Science
  Fund (FWF) grant No: F8512-N.'
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Christos
  full_name: Stefo, Christos
  id: a20e8902-32b0-11ee-9fa8-b23fa638b793
  last_name: Stefo
- first_name: Zhuolun
  full_name: Xiang, Zhuolun
  last_name: Xiang
- first_name: Eleftherios
  full_name: Kokoris Kogias, Eleftherios
  id: f5983044-d7ef-11ea-ac6d-fd1430a26d30
  last_name: Kokoris Kogias
citation:
  ama: 'Stefo C, Xiang Z, Kokoris Kogias E. Executing and proving over dirty ledgers.
    In: <i>27th International Conference on Financial Cryptography and Data Security</i>.
    Vol 13950. Springer Nature; 2023:3-20. doi:<a href="https://doi.org/10.1007/978-3-031-47754-6_1">10.1007/978-3-031-47754-6_1</a>'
  apa: 'Stefo, C., Xiang, Z., &#38; Kokoris Kogias, E. (2023). Executing and proving
    over dirty ledgers. In <i>27th International Conference on Financial Cryptography
    and Data Security</i> (Vol. 13950, pp. 3–20). Bol, Brac, Croatia: Springer Nature.
    <a href="https://doi.org/10.1007/978-3-031-47754-6_1">https://doi.org/10.1007/978-3-031-47754-6_1</a>'
  chicago: Stefo, Christos, Zhuolun Xiang, and Eleftherios Kokoris Kogias. “Executing
    and Proving over Dirty Ledgers.” In <i>27th International Conference on Financial
    Cryptography and Data Security</i>, 13950:3–20. Springer Nature, 2023. <a href="https://doi.org/10.1007/978-3-031-47754-6_1">https://doi.org/10.1007/978-3-031-47754-6_1</a>.
  ieee: C. Stefo, Z. Xiang, and E. Kokoris Kogias, “Executing and proving over dirty
    ledgers,” in <i>27th International Conference on Financial Cryptography and Data
    Security</i>, Bol, Brac, Croatia, 2023, vol. 13950, pp. 3–20.
  ista: 'Stefo C, Xiang Z, Kokoris Kogias E. 2023. Executing and proving over dirty
    ledgers. 27th International Conference on Financial Cryptography and Data Security.
    FC: Financial Cryptography and Data Security, LNCS, vol. 13950, 3–20.'
  mla: Stefo, Christos, et al. “Executing and Proving over Dirty Ledgers.” <i>27th
    International Conference on Financial Cryptography and Data Security</i>, vol.
    13950, Springer Nature, 2023, pp. 3–20, doi:<a href="https://doi.org/10.1007/978-3-031-47754-6_1">10.1007/978-3-031-47754-6_1</a>.
  short: C. Stefo, Z. Xiang, E. Kokoris Kogias, in:, 27th International Conference
    on Financial Cryptography and Data Security, Springer Nature, 2023, pp. 3–20.
conference:
  end_date: 2023-05-05
  location: Bol, Brac, Croatia
  name: 'FC: Financial Cryptography and Data Security'
  start_date: 2023-05-01
date_created: 2024-01-08T09:17:38Z
date_published: 2023-12-01T00:00:00Z
date_updated: 2024-01-08T09:28:14Z
day: '01'
department:
- _id: ElKo
- _id: GradSch
doi: 10.1007/978-3-031-47754-6_1
intvolume: '     13950'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://eprint.iacr.org/2022/1554
month: '12'
oa: 1
oa_version: Preprint
page: 3-20
project:
- _id: 34a4ce89-11ca-11ed-8bc3-8cc37fb6e11f
  grant_number: F8512
  name: Secure Network and Hardware for Efficient Blockchains
publication: 27th International Conference on Financial Cryptography and Data Security
publication_identifier:
  eisbn:
  - '9783031477546'
  eissn:
  - 0302-9743
  isbn:
  - '9783031477539'
  issn:
  - 1611-3349
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Executing and proving over dirty ledgers
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13950
year: '2023'
...
---
_id: '7453'
abstract:
- lang: eng
  text: We illustrate the ingredients of the state-of-the-art of model-based approach
    for the formal design and verification of cyber-physical systems. To capture the
    interaction between a discrete controller and its continuously evolving environment,
    we use the formal models of timed and hybrid automata. We explain the steps of
    modeling and verification in the tools Uppaal and SpaceEx using a case study based
    on a dual-chamber implantable pacemaker monitoring a human heart. We show how
    to design a model as a composition of components, how to construct models at varying
    levels of detail, how to establish that one model is an abstraction of another,
    how to specify correctness requirements using temporal logic, and how to verify
    that a model satisfies a logical requirement.
acknowledgement: This research was supported in part by the Austrian Science Fund
  (FWF) under grants S11402-N23(RiSE/SHiNE) and Z211-N23 (Wittgenstein Award). This
  research has received funding from the Sino-Danish Basic Research Centre, IDEA4CPS,
  funded by the Danish National Research Foundation and the National Science Foundation,
  China, the Innovation Fund Denmark centre DiCyPS, as well as the ERC Advanced Grant
  LASSO.
alternative_title:
- Lecture Notes in Computer Science
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Mirco
  full_name: Giacobbe, Mirco
  id: 3444EA5E-F248-11E8-B48F-1D18A9856A87
  last_name: Giacobbe
  orcid: 0000-0001-8180-0904
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Kim G.
  full_name: Larsen, Kim G.
  last_name: Larsen
- first_name: Marius
  full_name: Mikučionis, Marius
  last_name: Mikučionis
citation:
  ama: 'Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. Continuous-time
    models for system design and analysis. In: Steffen B, Woeginger G, eds. <i>Computing
    and Software Science</i>. Vol 10000. LNCS. Springer Nature; 2019:452-477. doi:<a
    href="https://doi.org/10.1007/978-3-319-91908-9_22">10.1007/978-3-319-91908-9_22</a>'
  apa: Alur, R., Giacobbe, M., Henzinger, T. A., Larsen, K. G., &#38; Mikučionis,
    M. (2019). Continuous-time models for system design and analysis. In B. Steffen
    &#38; G. Woeginger (Eds.), <i>Computing and Software Science</i> (Vol. 10000,
    pp. 452–477). Springer Nature. <a href="https://doi.org/10.1007/978-3-319-91908-9_22">https://doi.org/10.1007/978-3-319-91908-9_22</a>
  chicago: Alur, Rajeev, Mirco Giacobbe, Thomas A Henzinger, Kim G. Larsen, and Marius
    Mikučionis. “Continuous-Time Models for System Design and Analysis.” In <i>Computing
    and Software Science</i>, edited by Bernhard Steffen and Gerhard Woeginger, 10000:452–77.
    LNCS. Springer Nature, 2019. <a href="https://doi.org/10.1007/978-3-319-91908-9_22">https://doi.org/10.1007/978-3-319-91908-9_22</a>.
  ieee: R. Alur, M. Giacobbe, T. A. Henzinger, K. G. Larsen, and M. Mikučionis, “Continuous-time
    models for system design and analysis,” in <i>Computing and Software Science</i>,
    vol. 10000, B. Steffen and G. Woeginger, Eds. Springer Nature, 2019, pp. 452–477.
  ista: 'Alur R, Giacobbe M, Henzinger TA, Larsen KG, Mikučionis M. 2019.Continuous-time
    models for system design and analysis. In: Computing and Software Science. Lecture
    Notes in Computer Science, vol. 10000, 452–477.'
  mla: Alur, Rajeev, et al. “Continuous-Time Models for System Design and Analysis.”
    <i>Computing and Software Science</i>, edited by Bernhard Steffen and Gerhard
    Woeginger, vol. 10000, Springer Nature, 2019, pp. 452–77, doi:<a href="https://doi.org/10.1007/978-3-319-91908-9_22">10.1007/978-3-319-91908-9_22</a>.
  short: R. Alur, M. Giacobbe, T.A. Henzinger, K.G. Larsen, M. Mikučionis, in:, B.
    Steffen, G. Woeginger (Eds.), Computing and Software Science, Springer Nature,
    2019, pp. 452–477.
date_created: 2020-02-05T10:51:44Z
date_published: 2019-10-05T00:00:00Z
date_updated: 2022-09-06T08:25:52Z
day: '05'
department:
- _id: ToHe
doi: 10.1007/978-3-319-91908-9_22
editor:
- first_name: Bernhard
  full_name: Steffen, Bernhard
  last_name: Steffen
- first_name: Gerhard
  full_name: Woeginger, Gerhard
  last_name: Woeginger
intvolume: '     10000'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://doi.org/10.1007/978-3-319-91908-9_22
month: '10'
oa: 1
oa_version: Published Version
page: 452-477
project:
- _id: 25F2ACDE-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S11402-N23
  name: Rigorous Systems Engineering
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Computing and Software Science
publication_identifier:
  eisbn:
  - '9783319919089'
  eissn:
  - 0302-9743
  isbn:
  - '9783319919072'
  issn:
  - 1611-3349
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: Continuous-time models for system design and analysis
type: book_chapter
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10000
year: '2019'
...