---
_id: '4440'
abstract:
- lang: eng
text: We present a methodology for proving temporal properties of the divergent
runs of reactive systems with real-valued clocks. A run diverges if time advances
beyond any bound. Since the divergent runs of a system may satisfy liveness properties
that are not satisfied by some convergent runs, the standard proof rules are incomplete
if only divergent runs are considered. First, we develop a sound and complete
proof calculus for divergence, which is based on translating clock systems into
discrete systems. Then, we show that simpler proofs can be obtained for stronger
divergence assumptions, such as unknown -divergence, which requires that all delays
have a minimum duration of some unknown constant . We classify all real-time systems
into an infinite hierarchy, according to how well they admit the translation of
eventuality properties into equivalent safety properties.
acknowledgement: Supported in part by the National Science Foundation under grant
CCR-9200794, by the United States Air Force Office of Scientific Research under
contract F49620- 93-1-0056, and by the Defense Advanced Research Projects Agency
under grant NAG2-892.
alternative_title:
- LNCS
article_processing_charge: No
author:
- 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: Peter
full_name: Kopke, Peter
last_name: Kopke
citation:
ama: 'Henzinger TA, Kopke P. Verification methods for the divergent runs of clock
systems. In: 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. Vol 863. Springer; 1994:351-372. doi:10.1007/3-540-58468-4_173'
apa: 'Henzinger, T. A., & Kopke, P. (1994). Verification methods for the divergent
runs of clock systems. In 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems (Vol. 863, pp. 351–372). Lübeck, Gernany:
Springer. https://doi.org/10.1007/3-540-58468-4_173'
chicago: Henzinger, Thomas A, and Peter Kopke. “Verification Methods for the Divergent
Runs of Clock Systems.” In 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems, 863:351–72. Springer, 1994. https://doi.org/10.1007/3-540-58468-4_173.
ieee: T. A. Henzinger and P. Kopke, “Verification methods for the divergent runs
of clock systems,” in 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems, Lübeck, Gernany, 1994, vol. 863, pp. 351–372.
ista: 'Henzinger TA, Kopke P. 1994. Verification methods for the divergent runs
of clock systems. 3rd International Symposium on Formal Techniques in Real-Time
and Fault-Tolerant Systems. FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant
Systems, LNCS, vol. 863, 351–372.'
mla: Henzinger, Thomas A., and Peter Kopke. “Verification Methods for the Divergent
Runs of Clock Systems.” 3rd International Symposium on Formal Techniques in
Real-Time and Fault-Tolerant Systems, vol. 863, Springer, 1994, pp. 351–72,
doi:10.1007/3-540-58468-4_173.
short: T.A. Henzinger, P. Kopke, in:, 3rd International Symposium on Formal Techniques
in Real-Time and Fault-Tolerant Systems, Springer, 1994, pp. 351–372.
conference:
end_date: 1994-09-23
location: Lübeck, Gernany
name: 'FTRTFT: Formal Techniques in Real-Time and Fault-Tolerant Systems'
start_date: 1994-09-19
date_created: 2018-12-11T12:08:52Z
date_published: 1994-01-01T00:00:00Z
date_updated: 2022-06-02T09:35:58Z
day: '01'
doi: 10.1007/3-540-58468-4_173
extern: '1'
intvolume: ' 863'
language:
- iso: eng
main_file_link:
- url: https://link.springer.com/chapter/10.1007/3-540-58468-4_173
month: '01'
oa_version: None
page: 351 - 372
publication: 3rd International Symposium on Formal Techniques in Real-Time and Fault-Tolerant
Systems
publication_status: published
publisher: Springer
publist_id: '287'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Verification methods for the divergent runs of clock systems
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 863
year: '1994'
...
---
_id: '4501'
abstract:
- lang: eng
text: 'We extend the specification language of temporal logic, the corresponding
verification framework, and the underlying computational model to deal with real-;time
properties of reactive systems. The abstract notion of timed transition systems
generalizes traditional transition systems conservatively: qualitative fairness
requirements are replaced (and superseded) by quantitative lower-bound and upper-bound
timing constraints on transitions. This framework can model real-time systems
that communicate either through shared variables or by message passing and real-time
issues such as timeouts, process priorities (interrupts), and process scheduling.
We exhibit two styles for the specification of real-time systems. While the first
approach uses time-bounded versions of the temporal operators, the second approach
allows explicit references to time through a special clock variable. Corresponding
to the two styles of specification, we present and compare two different proof
methodologies for the verification of timing requirements that are expressed in
these styles. For the bounded-operator style, we provide a set of proof rules
for establishing bounded-invariance and bounded-responce properties of timed transition
systems. This approach generalizes the standard temporal proof rules for verifying
invariance and response properties conservatively. For the explicit-clock style,
we exploit the observation that every time-bounded property is a safety property
and use the standard temporal proof rules for establishing safety properties.'
acknowledgement: 'This research was supported in part by an IBM graduate fellowship,
by the National Science Foundation under Grants CCR-9223226 and CCR-9200794. by
the Defense Advanced Research Projects Agency under Contract N00039-84-C-0211. by
the United States Air Force OMee of Scientific Research under Contracts F49620-93-141139
and F4962043-1-0056. and by the European Community ESPRIT Basic Research Action
Project 6021 (REACT). A preliminary version of Part 1 of this paper appeared in
the proceedings of the 1991 REX Workshop on Real Time Theory In Prate [HMP92a I
a preliminary version of Part II appeared in the proceedings of the 1991 ACM Symposium
on Principles of Programming Languages RIMP911. '
article_processing_charge: No
article_type: original
author:
- 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: Zohar
full_name: Manna, Zohar
last_name: Manna
- first_name: Amir
full_name: Pnueli, Amir
last_name: Pnueli
citation:
ama: Henzinger TA, Manna Z, Pnueli A. Temporal proof methodologies for timed transition
systems. Information and Computation. 1994;112(2):273-337. doi:10.1006/inco.1994.1060
apa: Henzinger, T. A., Manna, Z., & Pnueli, A. (1994). Temporal proof methodologies
for timed transition systems. Information and Computation. Elsevier. https://doi.org/10.1006/inco.1994.1060
chicago: Henzinger, Thomas A, Zohar Manna, and Amir Pnueli. “Temporal Proof Methodologies
for Timed Transition Systems.” Information and Computation. Elsevier, 1994.
https://doi.org/10.1006/inco.1994.1060.
ieee: T. A. Henzinger, Z. Manna, and A. Pnueli, “Temporal proof methodologies for
timed transition systems,” Information and Computation, vol. 112, no. 2.
Elsevier, pp. 273–337, 1994.
ista: Henzinger TA, Manna Z, Pnueli A. 1994. Temporal proof methodologies for timed
transition systems. Information and Computation. 112(2), 273–337.
mla: Henzinger, Thomas A., et al. “Temporal Proof Methodologies for Timed Transition
Systems.” Information and Computation, vol. 112, no. 2, Elsevier, 1994,
pp. 273–337, doi:10.1006/inco.1994.1060.
short: T.A. Henzinger, Z. Manna, A. Pnueli, Information and Computation 112 (1994)
273–337.
date_created: 2018-12-11T12:09:10Z
date_published: 1994-08-01T00:00:00Z
date_updated: 2022-06-02T09:24:58Z
day: '01'
doi: 10.1006/inco.1994.1060
extern: '1'
intvolume: ' 112'
issue: '2'
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://www.sciencedirect.com/science/article/pii/S0890540184710601?via%3Dihub
month: '08'
oa: 1
oa_version: None
page: 273 - 337
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '227'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Temporal proof methodologies for timed transition systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 112
year: '1994'
...
---
_id: '4503'
abstract:
- lang: eng
text: 'We describe finite-state programs over real-numbered time in a guarded-command
language with real-valued clocks or, equivalently, as finite automata with real-valued
clocks. Model checking answers the question which states of a real-time program
satisfy a branching-time specification (given in an extension of CTL with clock
variables). We develop an algorithm that computes this set of states symbolically
as a fixpoint of a functional on state predicates, without constructing the state
space. For this purpose, we introduce a μ-calculus on computation trees over real-numbered
time. Unfortunately, many standard program properties, such as response for all
nonzeno execution sequences (during which time diverges), cannot be characterized
by fixpoints: we show that the expressiveness of the timed μ-calculus is incomparable
to the expressiveness of timed CTL. Fortunately, this result does not impair the
symbolic verification of "implementable" real-time programs-those whose
safety constraints are machine-closed with respect to diverging time and whose
fairness constraints are restricted to finite upper bounds on clock values. All
timed CTL properties of such programs are shown to be computable as finitely approximable
fixpoints in a simple decidable theory.'
acknowledgement: We thank Peter Kopke for a careful reading.
article_processing_charge: No
article_type: original
author:
- 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: Xavier
full_name: Nicollin, Xavier
last_name: Nicollin
- first_name: Joseph
full_name: Sifakis, Joseph
last_name: Sifakis
- first_name: Sergio
full_name: Yovine, Sergio
last_name: Yovine
citation:
ama: Henzinger TA, Nicollin X, Sifakis J, Yovine S. Symbolic model checking for
real-time systems. Information and Computation. 1994;111(2):193-244. doi:10.1006/inco.1994.1045
apa: Henzinger, T. A., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic
model checking for real-time systems. Information and Computation. Elsevier.
https://doi.org/10.1006/inco.1994.1045
chicago: Henzinger, Thomas A, Xavier Nicollin, Joseph Sifakis, and Sergio Yovine.
“Symbolic Model Checking for Real-Time Systems.” Information and Computation.
Elsevier, 1994. https://doi.org/10.1006/inco.1994.1045.
ieee: T. A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, “Symbolic model checking
for real-time systems,” Information and Computation, vol. 111, no. 2. Elsevier,
pp. 193–244, 1994.
ista: Henzinger TA, Nicollin X, Sifakis J, Yovine S. 1994. Symbolic model checking
for real-time systems. Information and Computation. 111(2), 193–244.
mla: Henzinger, Thomas A., et al. “Symbolic Model Checking for Real-Time Systems.”
Information and Computation, vol. 111, no. 2, Elsevier, 1994, pp. 193–244,
doi:10.1006/inco.1994.1045.
short: T.A. Henzinger, X. Nicollin, J. Sifakis, S. Yovine, Information and Computation
111 (1994) 193–244.
date_created: 2018-12-11T12:09:11Z
date_published: 1994-06-01T00:00:00Z
date_updated: 2022-06-02T09:02:02Z
day: '01'
doi: 10.1006/inco.1994.1045
extern: '1'
intvolume: ' 111'
issue: '2'
language:
- iso: eng
main_file_link:
- url: https://www.sciencedirect.com/science/article/pii/S0890540184710455?via%3Dihub
month: '06'
oa_version: None
page: 193 - 244
publication: Information and Computation
publication_identifier:
issn:
- 0890-5401
publication_status: published
publisher: Elsevier
publist_id: '226'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Symbolic model checking for real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 111
year: '1994'
...