---
_id: '4409'
abstract:
- lang: eng
  text: "Models of timed systems must incorporate not only the sequence of system
    events, but the timings of these events as well to capture the real-time aspects
    of physical systems. Timed automata are models of real-time systems in which states
    consist of discrete locations and values for real-time clocks. The presence of
    real-time clocks leads to an uncountable state space. This thesis studies verification
    problems on timed automata in a game theoretic framework.\r\n\r\nFor untimed systems,
    two systems are close if every sequence of events of one system is also observable
    in the second system. For timed systems, the difference in timings of the two
    corresponding sequences is also of importance. We propose the notion of bisimulation
    distance which quantifies timing differences; if the bisimulation distance between
    two systems is epsilon, then (a) every sequence of events of one system has a
    corresponding matching sequence in the other, and (b) the timings of matching
    events in between the two corresponding traces do not differ by more than epsilon.
    We show that we can compute the bisimulation distance between two timed automata
    to within any desired degree of accuracy. We also show that the timed verification
    logic TCTL is robust with respect to our notion of quantitative bisimilarity,
    in particular, if a system satisfies a formula, then every close system satisfies
    a close formula.\r\n\r\nTimed games are used for distinguishing between the actions
    of several agents, typically a controller and an environment. The controller must
    achieve its objective against all possible choices of the environment. The modeling
    of the passage of time leads to the presence of zeno executions, and corresponding
    unrealizable strategies of the controller which may achieve objectives by blocking
    time. We disallow such unreasonable strategies by restricting all agents to use
    only receptive strategies --strategies which while not being required to ensure
    time divergence by any agent, are such that no agent is responsible for blocking
    time. Time divergence is guaranteed when all players use receptive strategies.
    We show that timed automaton games with receptive strategies can be solved by
    a reduction to finite state turn based game graphs. We define the logic timed
    alternating-time temporal logic for verification of timed automaton games and
    show that the logic can be model checked in EXPTIME. We also show that the minimum
    time required by an agent to reach a desired location, and the maximum time an
    agent can stay safe within a set of locations, against all possible actions of
    its adversaries are both computable.\r\n\r\nWe next study the memory requirements
    of winning strategies for timed automaton games. We prove that finite memory strategies
    suffice for safety objectives, and that winning strategies for reachability objectives
    may require infinite memory in general. We introduce randomized strategies in
    which an agent can propose a probabilistic distribution of moves and show that
    finite memory randomized strategies suffice for all omega-regular objectives.
    We also show that while randomization helps in simplifying winning strategies,
    and thus allows the construction of simpler controllers, it does not help a player
    in winning at more states, and thus does not allow the construction of more powerful
    controllers.\r\n\r\nFinally we study robust winning strategies in timed games.
    In a physical system, a controller may propose an action together with a time
    delay, but the action cannot be assumed to be executed at the exact proposed time
    delay. We present robust strategies which incorporate such jitters and show that
    the set of states from which an agent can win robustly is computable."
article_processing_charge: No
author:
- first_name: Vinayak
  full_name: Prabhu, Vinayak
  last_name: Prabhu
citation:
  ama: Prabhu V. Games for the verification of timed systems. 2008:1-137.
  apa: Prabhu, V. (2008). <i>Games for the verification of timed systems</i>. University
    of California, Berkeley.
  chicago: Prabhu, Vinayak. “Games for the Verification of Timed Systems.” University
    of California, Berkeley, 2008.
  ieee: V. Prabhu, “Games for the verification of timed systems,” University of California,
    Berkeley, 2008.
  ista: Prabhu V. 2008. Games for the verification of timed systems. University of
    California, Berkeley.
  mla: Prabhu, Vinayak. <i>Games for the Verification of Timed Systems</i>. University
    of California, Berkeley, 2008, pp. 1–137.
  short: V. Prabhu, Games for the Verification of Timed Systems, University of California,
    Berkeley, 2008.
date_created: 2018-12-11T12:08:42Z
date_published: 2008-09-01T00:00:00Z
date_updated: 2022-02-14T14:35:11Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2008/EECS-2008-97.html
month: '09'
oa: 1
oa_version: None
page: 1 - 137
publication_status: published
publisher: University of California, Berkeley
publist_id: '319'
status: public
supervisor:
- 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: John
  full_name: Steel, John
  last_name: Steel
- first_name: Pravin
  full_name: Varaiya, Pravin
  last_name: Varaiya
title: Games for the verification of timed systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_id: '4415'
abstract:
- lang: eng
  text: 'Many computing applications, especially those in safety critical embedded
    systems, require highly predictable timing properties. However, time is often
    not present in the prevailing computing and networking abstractions. In fact,
    most advances in computer architecture, software, and networking favor average-case
    performance over timing predictability. This thesis studies several methods for
    the design of concurrent and/or distributed embedded systems with precise timing
    guarantees. The focus is on flexible and compositional methods for programming
    and verification of the timing properties. The presented methods together with
    related formalisms cover two levels of design: (1) Programming language/model
    level. We propose the distributed variant of Giotto, a coordination programming
    language with an explicit temporal semantics—the logical execution time (LET)
    semantics. The LET of a task is an interval of time that specifies the time instants
    at which task inputs and outputs become available (task release and termination
    instants). The LET of a task is always non-zero. This allows us to communicate
    values across the network without changing the timing information of the task,
    and without introducing nondeterminism. We show how this methodology supports
    distributed code generation for distributed real-time systems. The method gives
    up some performance in favor of composability and predictability. We characterize
    the tradeoff by comparing the LET semantics with the semantics used in Simulink.
    (2) Abstract task graph level. We study interface-based design and verification
    of applications represented with task graphs. We consider task sequence graphs
    with general event models, and cyclic graphs with periodic event models with jitter
    and phase. Here an interface of a component exposes time and resource constraints
    of the component. Together with interfaces we formally define interface composition
    operations and the refinement relation. For efficient and flexible composability
    checking two properties are important: incremental design and independent refinement.
    According to the incremental design property the composition of interfaces can
    be performed in any order, even if interfaces for some components are not known.
    The refinement relation is defined such that in a design we can always substitute
    a refined interface for an abstract one. We show that the framework supports independent
    refinement, i.e., the refinement relation is preserved under composition operations.'
acknowledgement: 978-0-549-83480-9
article_processing_charge: No
author:
- first_name: Slobodan
  full_name: Matic, Slobodan
  last_name: Matic
citation:
  ama: Matic S. Compositionality in deterministic real-time embedded systems. 2008:1-148.
  apa: Matic, S. (2008). <i>Compositionality in deterministic real-time embedded systems</i>.
    University of California, Berkeley.
  chicago: Matic, Slobodan. “Compositionality in Deterministic Real-Time Embedded
    Systems.” University of California, Berkeley, 2008.
  ieee: S. Matic, “Compositionality in deterministic real-time embedded systems,”
    University of California, Berkeley, 2008.
  ista: Matic S. 2008. Compositionality in deterministic real-time embedded systems.
    University of California, Berkeley.
  mla: Matic, Slobodan. <i>Compositionality in Deterministic Real-Time Embedded Systems</i>.
    University of California, Berkeley, 2008, pp. 1–148.
  short: S. Matic, Compositionality in Deterministic Real-Time Embedded Systems, University
    of California, Berkeley, 2008.
date_created: 2018-12-11T12:08:44Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2022-02-14T14:08:50Z
day: '01'
degree_awarded: PhD
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 148
publication_status: published
publisher: University of California, Berkeley
publist_id: '316'
status: public
supervisor:
- 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: Edward
  full_name: Lee, Edward
  last_name: Lee
- first_name: Raja
  full_name: Sengupta, Raja
  last_name: Sengupta
title: Compositionality in deterministic real-time embedded systems
type: dissertation
user_id: 8b945eb4-e2f2-11eb-945a-df72226e66a9
year: '2008'
...
---
_id: '4452'
abstract:
- lang: eng
  text: We describe Valigator, a software tool for imperative program verification
    that efficiently combines symbolic computation and automated reasoning in a uniform
    framework. The system offers support for automatically generating and proving
    verification conditions and, most importantly, for automatically inferring loop
    invariants and bound assertions by means of symbolic summation, Gröbner basis
    computation, and quantifier elimination. We present general principles of the
    implementation and illustrate them on examples.
acknowledgement: This research was supported by the Swiss NSF.
alternative_title:
- LNCS
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Thibaud
  full_name: Hottelier, Thibaud
  last_name: Hottelier
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
citation:
  ama: 'Henzinger TA, Hottelier T, Kovács L. Valigator: A verification tool with bound
    and invariant generation. In: Vol 5330. Springer; 2008:333-342. doi:<a href="https://doi.org/10.1007/978-3-540-89439-1_24">10.1007/978-3-540-89439-1_24</a>'
  apa: 'Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2008). Valigator: A verification
    tool with bound and invariant generation (Vol. 5330, pp. 333–342). Presented at
    the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Springer.
    <a href="https://doi.org/10.1007/978-3-540-89439-1_24">https://doi.org/10.1007/978-3-540-89439-1_24</a>'
  chicago: 'Henzinger, Thomas A, Thibaud Hottelier, and Laura Kovács. “Valigator:
    A Verification Tool with Bound and Invariant Generation,” 5330:333–42. Springer,
    2008. <a href="https://doi.org/10.1007/978-3-540-89439-1_24">https://doi.org/10.1007/978-3-540-89439-1_24</a>.'
  ieee: 'T. A. Henzinger, T. Hottelier, and L. Kovács, “Valigator: A verification
    tool with bound and invariant generation,” presented at the LPAR: Logic for Programming,
    Artificial Intelligence, and Reasoning, 2008, vol. 5330, pp. 333–342.'
  ista: 'Henzinger TA, Hottelier T, Kovács L. 2008. Valigator: A verification tool
    with bound and invariant generation. LPAR: Logic for Programming, Artificial Intelligence,
    and Reasoning, LNCS, vol. 5330, 333–342.'
  mla: 'Henzinger, Thomas A., et al. <i>Valigator: A Verification Tool with Bound
    and Invariant Generation</i>. Vol. 5330, Springer, 2008, pp. 333–42, doi:<a href="https://doi.org/10.1007/978-3-540-89439-1_24">10.1007/978-3-540-89439-1_24</a>.'
  short: T.A. Henzinger, T. Hottelier, L. Kovács, in:, Springer, 2008, pp. 333–342.
conference:
  name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
date_created: 2018-12-11T12:08:55Z
date_published: 2008-11-13T00:00:00Z
date_updated: 2021-01-12T07:57:04Z
day: '13'
doi: 10.1007/978-3-540-89439-1_24
extern: 1
intvolume: '      5330'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/valigator.pdf
month: '11'
page: 333 - 342
publication_status: published
publisher: Springer
publist_id: '277'
quality_controlled: 0
status: public
title: 'Valigator: A verification tool with bound and invariant generation'
type: conference
volume: 5330
year: '2008'
...
---
_id: '4509'
abstract:
- lang: eng
  text: 'I discuss two main challenges in embedded systems design: the challenge to
    build predictable systems, and that to build robust systems. I suggest how predictability
    can be formalized as a form of determinism, and robustness as a form of continuity.'
author:
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: 'Henzinger TA. Two challenges in embedded systems design: Predictability and
    robustness. <i>Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences</i>. 2008;366(1881):3727-3736. doi:<a href="https://doi.org/10.1098/rsta.2008.0141">10.1098/rsta.2008.0141</a>'
  apa: 'Henzinger, T. A. (2008). Two challenges in embedded systems design: Predictability
    and robustness. <i>Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences</i>. Royal Society of London. <a href="https://doi.org/10.1098/rsta.2008.0141">https://doi.org/10.1098/rsta.2008.0141</a>'
  chicago: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
    and Robustness.” <i>Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences</i>. Royal Society of London, 2008. <a href="https://doi.org/10.1098/rsta.2008.0141">https://doi.org/10.1098/rsta.2008.0141</a>.'
  ieee: 'T. A. Henzinger, “Two challenges in embedded systems design: Predictability
    and robustness,” <i>Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences</i>, vol. 366, no. 1881. Royal Society of London,
    pp. 3727–3736, 2008.'
  ista: 'Henzinger TA. 2008. Two challenges in embedded systems design: Predictability
    and robustness. Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences. 366(1881), 3727–3736.'
  mla: 'Henzinger, Thomas A. “Two Challenges in Embedded Systems Design: Predictability
    and Robustness.” <i>Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences</i>, vol. 366, no. 1881, Royal Society of London,
    2008, pp. 3727–36, doi:<a href="https://doi.org/10.1098/rsta.2008.0141">10.1098/rsta.2008.0141</a>.'
  short: T.A. Henzinger, Philosophical Transactions of the Royal Society A Mathematical
    Physical and Engineering Sciences 366 (2008) 3727–3736.
date_created: 2018-12-11T12:09:13Z
date_published: 2008-07-31T00:00:00Z
date_updated: 2021-01-12T07:59:19Z
day: '31'
doi: 10.1098/rsta.2008.0141
extern: 1
intvolume: '       366'
issue: '1881'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/two_challenges_in_embedded_systems_design.pdf
month: '07'
page: 3727 - 3736
publication: Philosophical Transactions of the Royal Society A Mathematical Physical
  and Engineering Sciences
publication_status: published
publisher: Royal Society of London
publist_id: '219'
quality_controlled: 0
status: public
title: 'Two challenges in embedded systems design: Predictability and robustness'
type: journal_article
volume: 366
year: '2008'
...
---
_id: '4521'
abstract:
- lang: eng
  text: The search for proof and the search for counterexamples (bugs) are complementary
    activities that need to be pursued concurrently in order to maximize the practical
    success rate of verification tools.While this is well-understood in safety verification,
    the current focus of liveness verification has been almost exclusively on the
    search for termination proofs. A counterexample to termination is an infinite
    programexecution. In this paper, we propose a method to search for such counterexamples.
    The search proceeds in two phases. We first dynamically enumerate lasso-shaped
    candidate paths for counterexamples, and then statically prove their feasibility.
    We illustrate the utility of our nontermination prover, called TNT, on several
    nontrivial examples, some of which require bit-level reasoning about integer representations.
author:
- first_name: Ashutosh
  full_name: Ashutosh Gupta
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Andrey
  full_name: Rybalchenko, Andrey
  last_name: Rybalchenko
- first_name: Ru
  full_name: Xu, Ru-Gang
  last_name: Xu
citation:
  ama: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. Proving non-termination.
    In: ACM; 2008:147-158. doi:<a href="https://doi.org/10.1145/1328438.1328459">10.1145/1328438.1328459</a>'
  apa: 'Gupta, A., Henzinger, T. A., Majumdar, R., Rybalchenko, A., &#38; Xu, R. (2008).
    Proving non-termination (pp. 147–158). Presented at the POPL: Principles of Programming
    Languages, ACM. <a href="https://doi.org/10.1145/1328438.1328459">https://doi.org/10.1145/1328438.1328459</a>'
  chicago: Gupta, Ashutosh, Thomas A Henzinger, Ritankar Majumdar, Andrey Rybalchenko,
    and Ru Xu. “Proving Non-Termination,” 147–58. ACM, 2008. <a href="https://doi.org/10.1145/1328438.1328459">https://doi.org/10.1145/1328438.1328459</a>.
  ieee: 'A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu, “Proving
    non-termination,” presented at the POPL: Principles of Programming Languages,
    2008, pp. 147–158.'
  ista: 'Gupta A, Henzinger TA, Majumdar R, Rybalchenko A, Xu R. 2008. Proving non-termination.
    POPL: Principles of Programming Languages, 147–158.'
  mla: Gupta, Ashutosh, et al. <i>Proving Non-Termination</i>. ACM, 2008, pp. 147–58,
    doi:<a href="https://doi.org/10.1145/1328438.1328459">10.1145/1328438.1328459</a>.
  short: A. Gupta, T.A. Henzinger, R. Majumdar, A. Rybalchenko, R. Xu, in:, ACM, 2008,
    pp. 147–158.
conference:
  name: 'POPL: Principles of Programming Languages'
date_created: 2018-12-11T12:09:17Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:25Z
day: '01'
doi: 10.1145/1328438.1328459
extern: 1
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/proving_non-termination.pdf
month: '01'
page: 147 - 158
publication_status: published
publisher: ACM
publist_id: '208'
quality_controlled: 0
status: public
title: Proving non-termination
type: conference
year: '2008'
...
---
_id: '4524'
abstract:
- lang: eng
  text: "Complex requirements, time-to-market pressure and regulatory constraints
    have made the designing of embedded systems extremely challenging. This is evident
    by the increase in effort and expenditure for design of safety-driven real-time
    control-dominated applications like automotive and avionic controllers. Design
    processes are often challenged by lack of proper programming tools for specifying
    and verifying critical requirements (e.g. timing and reliability) of such applications.
    Platform based design, an approach for designing embedded systems, addresses the
    above concerns by separating requirement from architecture. The requirement specifies
    the intended behavior of an application while the architecture specifies the guarantees
    (e.g. execution speed, failure rate etc). An implementation, a mapping of the
    requirement on the architecture, is then analyzed for correctness. The orthogonalization
    of concerns makes the specification and analyses simpler. An effective use of
    such design methodology has been proposed in Logical Execution Time (LET) model
    of real-time tasks. The model separates the timing requirements (specified by
    release and termination instances of a task) from the architecture guarantees
    (specified by worst-case execution time of the task).\r\n\r\nThis dissertation
    proposes a coordination language, Hierarchical Timing Language (HTL), that captures
    the timing and reliability requirements of real-time applications. An implementation
    of the program on an architecture is then analyzed to check whether desired timing
    and reliability requirements are met or not. The core framework extends the LET
    model by accounting for reliability and refinement. The reliability model separates
    the reliability requirements of tasks from the reliability guarantees of the architecture.
    The requirement expresses the desired long-term reliability while the architecture
    provides a short-term reliability guarantee (e.g. failure rate for each iteration).
    The analysis checks if the short-term guarantee ensures the desired long-term
    reliability. The refinement model allows replacing a task by another task during
    program execution. Refinement preserves schedulability and reliability, i.e.,
    if a refined task is schedulable and reliable for an implementation, then the
    refining task is also schedulable and reliable for the implementation. Refinement
    helps in concise specification without overloading analysis.\r\n\r\nThe work presents
    the formal model, the analyses (both with and without refinement), and a compiler
    for HTL programs. The compiler checks composition and refinement constraints,
    performs schedulability and reliability analyses, and generates code for implementation
    of an HTL program on a virtual machine. Three real-time controllers, one each
    from automatic control, automotive control and avionic control, are used to illustrate
    the steps in modeling and analyzing HTL programs."
acknowledgement: 978-0-549-83679-7
article_processing_charge: No
author:
- first_name: Arkadeb
  full_name: Ghosal, Arkadeb
  last_name: Ghosal
citation:
  ama: Ghosal A. A hierarchical coordination language for reliable real-time tasks.
    2008:1-210.
  apa: Ghosal, A. (2008). <i>A hierarchical coordination language for reliable real-time
    tasks</i>. University of California, Berkeley.
  chicago: Ghosal, Arkadeb. “A Hierarchical Coordination Language for Reliable Real-Time
    Tasks.” University of California, Berkeley, 2008.
  ieee: A. Ghosal, “A hierarchical coordination language for reliable real-time tasks,”
    University of California, Berkeley, 2008.
  ista: Ghosal A. 2008. A hierarchical coordination language for reliable real-time
    tasks. University of California, Berkeley.
  mla: Ghosal, Arkadeb. <i>A Hierarchical Coordination Language for Reliable Real-Time
    Tasks</i>. University of California, Berkeley, 2008, pp. 1–210.
  short: A. Ghosal, A Hierarchical Coordination Language for Reliable Real-Time Tasks,
    University of California, Berkeley, 2008.
date_created: 2018-12-11T12:09:18Z
date_published: 2008-01-31T00:00:00Z
date_updated: 2021-01-12T07:59:26Z
day: '31'
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 1 - 210
publication_status: published
publisher: University of California, Berkeley
publist_id: '199'
status: public
supervisor:
- first_name: Alberto
  full_name: Sangiovanni-Vincentelli, Alberto
  last_name: Sangiovanni-Vincentelli
- 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: Edward
  full_name: Lee, Edward
  last_name: Lee
- first_name: Karl
  full_name: Hedrick, Karl
  last_name: Hedrick
title: A hierarchical coordination language for reliable real-time tasks
type: dissertation
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2008'
...
---
_id: '4527'
abstract:
- lang: eng
  text: |-
    We introduce bounded asynchrony, a notion of concurrency tailored to the modeling of biological cell-cell interactions. Bounded asynchrony is the result of a scheduler that bounds the number of steps that one process gets ahead of other processes; this allows the components of a system to move independently while keeping them coupled. Bounded asynchrony accurately reproduces the experimental observations made about certain cell-cell interactions: its constrained nondeterminism captures the variability observed in cells that, although equally potent, assume distinct fates. Real-life cells are not “scheduled”, but we show that distributed real-time behavior can lead to component interactions that are observationally equivalent to bounded asynchrony; this provides a possible mechanistic explanation for the phenomena observed during cell fate specification.
    We use model checking to determine cell fates. The nondeterminism of bounded asynchrony causes state explosion during model checking, but partial-order methods are not directly applicable. We present a new algorithm that reduces the number of states that need to be explored: our optimization takes advantage of the bounded-asynchronous progress and the spatially local interactions of components that model cells. We compare our own communication-based reduction with partial-order reduction (on a restricted form of bounded asynchrony) and experiments illustrate that our algorithm leads to significant savings.
acknowledgement: Supported in part by the Swiss National Science Foundation (grant
  205321-111840).
alternative_title:
- LNCS
author:
- first_name: Jasmin
  full_name: Fisher, Jasmin
  last_name: Fisher
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Maria
  full_name: Maria Mateescu
  id: 3B43276C-F248-11E8-B48F-1D18A9856A87
  last_name: Mateescu
- first_name: Nir
  full_name: Piterman, Nir
  last_name: Piterman
citation:
  ama: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. Bounded asynchrony: Concurrency
    for modeling cell-cell interactions. In: Vol 5054. Springer; 2008:17-32. doi:<a
    href="https://doi.org/10.1007/978-3-540-68413-8_2">10.1007/978-3-540-68413-8_2</a>'
  apa: 'Fisher, J., Henzinger, T. A., Mateescu, M., &#38; Piterman, N. (2008). Bounded
    asynchrony: Concurrency for modeling cell-cell interactions (Vol. 5054, pp. 17–32).
    Presented at the FMSB: Formal Methods in Systems Biology, Springer. <a href="https://doi.org/10.1007/978-3-540-68413-8_2">https://doi.org/10.1007/978-3-540-68413-8_2</a>'
  chicago: 'Fisher, Jasmin, Thomas A Henzinger, Maria Mateescu, and Nir Piterman.
    “Bounded Asynchrony: Concurrency for Modeling Cell-Cell Interactions,” 5054:17–32.
    Springer, 2008. <a href="https://doi.org/10.1007/978-3-540-68413-8_2">https://doi.org/10.1007/978-3-540-68413-8_2</a>.'
  ieee: 'J. Fisher, T. A. Henzinger, M. Mateescu, and N. Piterman, “Bounded asynchrony:
    Concurrency for modeling cell-cell interactions,” presented at the FMSB: Formal
    Methods in Systems Biology, 2008, vol. 5054, pp. 17–32.'
  ista: 'Fisher J, Henzinger TA, Mateescu M, Piterman N. 2008. Bounded asynchrony:
    Concurrency for modeling cell-cell interactions. FMSB: Formal Methods in Systems
    Biology, LNCS, vol. 5054, 17–32.'
  mla: 'Fisher, Jasmin, et al. <i>Bounded Asynchrony: Concurrency for Modeling Cell-Cell
    Interactions</i>. Vol. 5054, Springer, 2008, pp. 17–32, doi:<a href="https://doi.org/10.1007/978-3-540-68413-8_2">10.1007/978-3-540-68413-8_2</a>.'
  short: J. Fisher, T.A. Henzinger, M. Mateescu, N. Piterman, in:, Springer, 2008,
    pp. 17–32.
conference:
  name: 'FMSB: Formal Methods in Systems Biology'
date_created: 2018-12-11T12:09:19Z
date_published: 2008-05-26T00:00:00Z
date_updated: 2021-01-12T07:59:27Z
day: '26'
doi: 10.1007/978-3-540-68413-8_2
extern: 1
intvolume: '      5054'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/bounded_asynchrony.pdf
month: '05'
page: 17 - 32
publication_status: published
publisher: Springer
publist_id: '196'
quality_controlled: 0
status: public
title: 'Bounded asynchrony: Concurrency for modeling cell-cell interactions'
type: conference
volume: 5054
year: '2008'
...
---
_id: '4532'
abstract:
- lang: eng
  text: We consider the equivalence problem for labeled Markov chains (LMCs), where
    each state is labeled with an observation. Two LMCs are equivalent if every finite
    sequence of observations has the same probability of occurrence in the two LMCs.
    We show that equivalence can be decided in polynomial time, using a reduction
    to the equivalence problem for probabilistic automata, which is known to be solvable
    in polynomial time. We provide an alternative algorithm to solve the equivalence
    problem, which is based on a new definition of bisimulation for probabilistic
    automata. We also extend the technique to decide the equivalence of weighted probabilistic
    automata.
author:
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Jean
  full_name: Raskin, Jean-François
  last_name: Raskin
citation:
  ama: Doyen L, Henzinger TA, Raskin J. Equivalence of labeled Markov chains. <i>International
    Journal of Foundations of Computer Science</i>. 2008;19(3):549-563. doi:<a href="https://doi.org/10.1142/S0129054108005814
    ">10.1142/S0129054108005814 </a>
  apa: Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2008). Equivalence of labeled
    Markov chains. <i>International Journal of Foundations of Computer Science</i>.
    World Scientific Publishing. <a href="https://doi.org/10.1142/S0129054108005814
    ">https://doi.org/10.1142/S0129054108005814 </a>
  chicago: Doyen, Laurent, Thomas A Henzinger, and Jean Raskin. “Equivalence of Labeled
    Markov Chains.” <i>International Journal of Foundations of Computer Science</i>.
    World Scientific Publishing, 2008. <a href="https://doi.org/10.1142/S0129054108005814
    ">https://doi.org/10.1142/S0129054108005814 </a>.
  ieee: L. Doyen, T. A. Henzinger, and J. Raskin, “Equivalence of labeled Markov chains,”
    <i>International Journal of Foundations of Computer Science</i>, vol. 19, no.
    3. World Scientific Publishing, pp. 549–563, 2008.
  ista: Doyen L, Henzinger TA, Raskin J. 2008. Equivalence of labeled Markov chains.
    International Journal of Foundations of Computer Science. 19(3), 549–563.
  mla: Doyen, Laurent, et al. “Equivalence of Labeled Markov Chains.” <i>International
    Journal of Foundations of Computer Science</i>, vol. 19, no. 3, World Scientific
    Publishing, 2008, pp. 549–63, doi:<a href="https://doi.org/10.1142/S0129054108005814
    ">10.1142/S0129054108005814 </a>.
  short: L. Doyen, T.A. Henzinger, J. Raskin, International Journal of Foundations
    of Computer Science 19 (2008) 549–563.
date_created: 2018-12-11T12:09:20Z
date_published: 2008-06-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: '10.1142/S0129054108005814 '
extern: 1
intvolume: '        19'
issue: '3'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/equivalence_of_labeled_markov_chains.pdf
month: '06'
page: 549 - 563
publication: International Journal of Foundations of Computer Science
publication_status: published
publisher: World Scientific Publishing
publist_id: '192'
quality_controlled: 0
status: public
title: Equivalence of labeled Markov chains
type: journal_article
volume: 19
year: '2008'
...
---
_id: '4533'
abstract:
- lang: eng
  text: Interface theories have been proposed to support incremental design and independent
    implementability. Incremental design means that the compatibility checking of
    interfaces can proceed for partial system descriptions, without knowing the interfaces
    of all components. Independent implementability means that compatible interfaces
    can be refined separately, maintaining compatibility. We show that these interface
    theories provide no formal support for component reuse, meaning that the same
    component cannot be used to implement several different interfaces in a design.
    We add a new operation to interface theories in order to support such reuse. For
    example, different interfaces for the same component may refer to different aspects
    such as functionality, timing, and power consumption. We give both stateless and
    stateful examples for interface theories with component reuse. To illustrate component
    reuse in interface-based design, we show how the stateful theory provides a natural
    framework for specifying and refining PCI bus clients.
author:
- first_name: Laurent
  full_name: Doyen, Laurent
  last_name: Doyen
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Barbara
  full_name: Jobstmann, Barbara
  last_name: Jobstmann
- first_name: Tatjana
  full_name: Tatjana Petrov
  id: 3D5811FC-F248-11E8-B48F-1D18A9856A87
  last_name: Petrov
  orcid: 0000-0002-9041-0905
citation:
  ama: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. Interface theories with component
    reuse. In: ACM; 2008:79-88. doi:<a href="https://doi.org/10.1145/1450058.1450070">10.1145/1450058.1450070</a>'
  apa: 'Doyen, L., Henzinger, T. A., Jobstmann, B., &#38; Petrov, T. (2008). Interface
    theories with component reuse (pp. 79–88). Presented at the EMSOFT: Embedded Software
    , ACM. <a href="https://doi.org/10.1145/1450058.1450070">https://doi.org/10.1145/1450058.1450070</a>'
  chicago: Doyen, Laurent, Thomas A Henzinger, Barbara Jobstmann, and Tatjana Petrov.
    “Interface Theories with Component Reuse,” 79–88. ACM, 2008. <a href="https://doi.org/10.1145/1450058.1450070">https://doi.org/10.1145/1450058.1450070</a>.
  ieee: 'L. Doyen, T. A. Henzinger, B. Jobstmann, and T. Petrov, “Interface theories
    with component reuse,” presented at the EMSOFT: Embedded Software , 2008, pp.
    79–88.'
  ista: 'Doyen L, Henzinger TA, Jobstmann B, Petrov T. 2008. Interface theories with
    component reuse. EMSOFT: Embedded Software , 79–88.'
  mla: Doyen, Laurent, et al. <i>Interface Theories with Component Reuse</i>. ACM,
    2008, pp. 79–88, doi:<a href="https://doi.org/10.1145/1450058.1450070">10.1145/1450058.1450070</a>.
  short: L. Doyen, T.A. Henzinger, B. Jobstmann, T. Petrov, in:, ACM, 2008, pp. 79–88.
conference:
  name: 'EMSOFT: Embedded Software '
date_created: 2018-12-11T12:09:21Z
date_published: 2008-10-01T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '01'
doi: 10.1145/1450058.1450070
extern: 1
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/interface_theories_with_component_reuse.pdf
month: '10'
page: 79 - 88
publication_status: published
publisher: ACM
publist_id: '193'
quality_controlled: 0
status: public
title: Interface theories with component reuse
type: conference
year: '2008'
...
---
_id: '4534'
abstract:
- lang: eng
  text: A stochastic graph game is played by two players on a game graph with probabilistic
    transitions. We consider stochastic graph games with ω-regular winning conditions
    specified as parity objectives, and mean-payoff (or limit-average) objectives.
    These games lie in NP ∩ coNP. We present a polynomial-time Turing reduction of
    stochastic parity games to stochastic mean-payoff games.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Chatterjee K, Henzinger TA. Reduction of stochastic parity to stochastic mean-payoff
    games. <i>Information Processing Letters</i>. 2008;106(1):1-7. doi:<a href="https://doi.org/10.1016/j.ipl.2007.08.035">10.1016/j.ipl.2007.08.035</a>
  apa: Chatterjee, K., &#38; Henzinger, T. A. (2008). Reduction of stochastic parity
    to stochastic mean-payoff games. <i>Information Processing Letters</i>. Elsevier.
    <a href="https://doi.org/10.1016/j.ipl.2007.08.035">https://doi.org/10.1016/j.ipl.2007.08.035</a>
  chicago: Chatterjee, Krishnendu, and Thomas A Henzinger. “Reduction of Stochastic
    Parity to Stochastic Mean-Payoff Games.” <i>Information Processing Letters</i>.
    Elsevier, 2008. <a href="https://doi.org/10.1016/j.ipl.2007.08.035">https://doi.org/10.1016/j.ipl.2007.08.035</a>.
  ieee: K. Chatterjee and T. A. Henzinger, “Reduction of stochastic parity to stochastic
    mean-payoff games,” <i>Information Processing Letters</i>, vol. 106, no. 1. Elsevier,
    pp. 1–7, 2008.
  ista: Chatterjee K, Henzinger TA. 2008. Reduction of stochastic parity to stochastic
    mean-payoff games. Information Processing Letters. 106(1), 1–7.
  mla: Chatterjee, Krishnendu, and Thomas A. Henzinger. “Reduction of Stochastic Parity
    to Stochastic Mean-Payoff Games.” <i>Information Processing Letters</i>, vol.
    106, no. 1, Elsevier, 2008, pp. 1–7, doi:<a href="https://doi.org/10.1016/j.ipl.2007.08.035">10.1016/j.ipl.2007.08.035</a>.
  short: K. Chatterjee, T.A. Henzinger, Information Processing Letters 106 (2008)
    1–7.
date_created: 2018-12-11T12:09:21Z
date_published: 2008-03-31T00:00:00Z
date_updated: 2021-01-12T07:59:30Z
day: '31'
doi: 10.1016/j.ipl.2007.08.035
extern: 1
intvolume: '       106'
issue: '1'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/reduction_of_stochastic_parity_to_stochastic_mean-payoff_games.pdf
month: '03'
page: 1 - 7
publication: Information Processing Letters
publication_status: published
publisher: Elsevier
publist_id: '188'
quality_controlled: 0
status: public
title: Reduction of stochastic parity to stochastic mean-payoff games
type: journal_article
volume: 106
year: '2008'
...
---
_id: '4546'
abstract:
- lang: eng
  text: We propose the notion of logical reliability for real-time program tasks that
    interact through periodically updated program variables. We describe a reliability
    analysis that checks if the given short-term (e.g., single-period) reliability
    of a program variable update in an implementation is sufficient to meet the logical
    reliability requirement (of the program variable) in the long run. We then present
    a notion of design by refinement where a task can be refined by another task that
    writes to program variables with less logical reliability. The resulting analysis
    can be combined with an incremental schedulability analysis for interacting real-time
    tasks proposed earlier for the Hierarchical Timing Language (HTL), a coordination
    language for distributed real-time systems. We implemented a logical-reliability-enhanced
    prototype of the compiler and runtime infrastructure for HTL.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Arkadeb
  full_name: Ghosal, Arkadeb
  last_name: Ghosal
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Daniel
  full_name: Iercan, Daniel
  last_name: Iercan
- first_name: Christoph
  full_name: Kirsch, Christoph M
  last_name: Kirsch
- first_name: Claudio
  full_name: Pinello, Claudio
  last_name: Pinello
- first_name: Alberto
  full_name: Sangiovanni-Vincentelli, Alberto
  last_name: Sangiovanni Vincentelli
citation:
  ama: 'Chatterjee K, Ghosal A, Henzinger TA, et al. Logical reliability of interacting
    real-time tasks. In: IEEE; 2008:909-914. doi:<a href="https://doi.org/10.1145/1403375.1403595">10.1145/1403375.1403595</a>'
  apa: 'Chatterjee, K., Ghosal, A., Henzinger, T. A., Iercan, D., Kirsch, C., Pinello,
    C., &#38; Sangiovanni Vincentelli, A. (2008). Logical reliability of interacting
    real-time tasks (pp. 909–914). Presented at the DATE: Design, Automation and Test
    in Europe, IEEE. <a href="https://doi.org/10.1145/1403375.1403595">https://doi.org/10.1145/1403375.1403595</a>'
  chicago: Chatterjee, Krishnendu, Arkadeb Ghosal, Thomas A Henzinger, Daniel Iercan,
    Christoph Kirsch, Claudio Pinello, and Alberto Sangiovanni Vincentelli. “Logical
    Reliability of Interacting Real-Time Tasks,” 909–14. IEEE, 2008. <a href="https://doi.org/10.1145/1403375.1403595">https://doi.org/10.1145/1403375.1403595</a>.
  ieee: 'K. Chatterjee <i>et al.</i>, “Logical reliability of interacting real-time
    tasks,” presented at the DATE: Design, Automation and Test in Europe, 2008, pp.
    909–914.'
  ista: 'Chatterjee K, Ghosal A, Henzinger TA, Iercan D, Kirsch C, Pinello C, Sangiovanni
    Vincentelli A. 2008. Logical reliability of interacting real-time tasks. DATE:
    Design, Automation and Test in Europe, 909–914.'
  mla: Chatterjee, Krishnendu, et al. <i>Logical Reliability of Interacting Real-Time
    Tasks</i>. IEEE, 2008, pp. 909–14, doi:<a href="https://doi.org/10.1145/1403375.1403595">10.1145/1403375.1403595</a>.
  short: K. Chatterjee, A. Ghosal, T.A. Henzinger, D. Iercan, C. Kirsch, C. Pinello,
    A. Sangiovanni Vincentelli, in:, IEEE, 2008, pp. 909–914.
conference:
  name: 'DATE: Design, Automation and Test in Europe'
date_created: 2018-12-11T12:09:25Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:36Z
day: '01'
doi: 10.1145/1403375.1403595
extern: 1
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/logical_reliability_of_interacting_real-time_tasks.pdf
month: '01'
page: 909 - 914
publication_status: published
publisher: IEEE
publist_id: '171'
quality_controlled: 0
status: public
title: Logical reliability of interacting real-time tasks
type: conference
year: '2008'
...
---
_id: '4548'
abstract:
- lang: eng
  text: The value of a finite-state two-player zero-sum stochastic game with limit-average
    payoff can be approximated to within ε in time exponential in a polynomial in
    the size of the game times polynomial in logarithmic in 1/ε, for all ε &gt; 0.
author:
- first_name: Krishnendu
  full_name: Krishnendu Chatterjee
  id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
  last_name: Chatterjee
  orcid: 0000-0002-4561-241X
- first_name: Ritankar
  full_name: Majumdar, Ritankar S
  last_name: Majumdar
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
citation:
  ama: Chatterjee K, Majumdar R, Henzinger TA. Stochastic limit-average games are
    in EXPTIME. <i>International Journal of Game Theory</i>. 2008;37(2):219-234. doi:<a
    href="https://doi.org/10.1007/s00182-007-0110-5">10.1007/s00182-007-0110-5</a>
  apa: Chatterjee, K., Majumdar, R., &#38; Henzinger, T. A. (2008). Stochastic limit-average
    games are in EXPTIME. <i>International Journal of Game Theory</i>. Springer. <a
    href="https://doi.org/10.1007/s00182-007-0110-5">https://doi.org/10.1007/s00182-007-0110-5</a>
  chicago: Chatterjee, Krishnendu, Ritankar Majumdar, and Thomas A Henzinger. “Stochastic
    Limit-Average Games Are in EXPTIME.” <i>International Journal of Game Theory</i>.
    Springer, 2008. <a href="https://doi.org/10.1007/s00182-007-0110-5">https://doi.org/10.1007/s00182-007-0110-5</a>.
  ieee: K. Chatterjee, R. Majumdar, and T. A. Henzinger, “Stochastic limit-average
    games are in EXPTIME,” <i>International Journal of Game Theory</i>, vol. 37, no.
    2. Springer, pp. 219–234, 2008.
  ista: Chatterjee K, Majumdar R, Henzinger TA. 2008. Stochastic limit-average games
    are in EXPTIME. International Journal of Game Theory. 37(2), 219–234.
  mla: Chatterjee, Krishnendu, et al. “Stochastic Limit-Average Games Are in EXPTIME.”
    <i>International Journal of Game Theory</i>, vol. 37, no. 2, Springer, 2008, pp.
    219–34, doi:<a href="https://doi.org/10.1007/s00182-007-0110-5">10.1007/s00182-007-0110-5</a>.
  short: K. Chatterjee, R. Majumdar, T.A. Henzinger, International Journal of Game
    Theory 37 (2008) 219–234.
date_created: 2018-12-11T12:09:25Z
date_published: 2008-01-01T00:00:00Z
date_updated: 2021-01-12T07:59:37Z
day: '01'
doi: 10.1007/s00182-007-0110-5
extern: 1
intvolume: '        37'
issue: '2'
main_file_link:
- open_access: '0'
  url: http://pub.ist.ac.at/%7Etah/Publications/stochastic_limit-average_games_are_in_exptime.pdf
month: '01'
page: 219 - 234
publication: International Journal of Game Theory
publication_status: published
publisher: Springer
publist_id: '168'
quality_controlled: 0
status: public
title: Stochastic limit-average games are in EXPTIME
type: journal_article
volume: 37
year: '2008'
...