---
_id: '9393'
abstract:
- lang: eng
text: "We consider the core algorithmic problems related to verification of systems
with respect to three classical quantitative properties, namely, the mean-payoff,
the ratio, and the minimum initial credit for energy property. The algorithmic
problem given a graph and a quantitative property asks to compute the optimal
value (the infimum value over all traces) from every node of the graph. We consider
graphs with bounded treewidth—a class that contains the control flow graphs of
most programs. Let n denote the number of nodes of a graph, m the number of edges
(for bounded treewidth \U0001D45A=\U0001D442(\U0001D45B)) and W the largest absolute
value of the weights. Our main theoretical results are as follows. First, for
the minimum initial credit problem we show that (1) for general graphs the problem
can be solved in \U0001D442(\U0001D45B2⋅\U0001D45A) time and the associated decision
problem in \U0001D442(\U0001D45B⋅\U0001D45A) time, improving the previous known
\U0001D442(\U0001D45B3⋅\U0001D45A⋅log(\U0001D45B⋅\U0001D44A)) and \U0001D442(\U0001D45B2⋅\U0001D45A)
bounds, respectively; and (2) for bounded treewidth graphs we present an algorithm
that requires \U0001D442(\U0001D45B⋅log\U0001D45B) time. Second, for bounded treewidth
graphs we present an algorithm that approximates the mean-payoff value within
a factor of 1+\U0001D716 in time \U0001D442(\U0001D45B⋅log(\U0001D45B/\U0001D716))
as compared to the classical exact algorithms on general graphs that require quadratic
time. Third, for the ratio property we present an algorithm that for bounded treewidth
graphs works in time \U0001D442(\U0001D45B⋅log(|\U0001D44E⋅\U0001D44F|))=\U0001D442(\U0001D45B⋅log(\U0001D45B⋅\U0001D44A)),
when the output is \U0001D44E\U0001D44F, as compared to the previously best known
algorithm on general graphs with running time \U0001D442(\U0001D45B2⋅log(\U0001D45B⋅\U0001D44A)).
We have implemented some of our algorithms and show that they present a significant
speedup on standard benchmarks."
acknowledgement: 'The research was partly supported by Austrian Science Fund (FWF)
Grant No P23499- N23, FWF NFN Grant No S11407-N23 (RiSE/SHiNE), ERC Start Grant
(279307: Graph Games), and Microsoft faculty fellows award.'
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Krishnendu
full_name: Chatterjee, Krishnendu
id: 2E5DCA20-F248-11E8-B48F-1D18A9856A87
last_name: Chatterjee
orcid: 0000-0002-4561-241X
- first_name: Rasmus
full_name: Ibsen-Jensen, Rasmus
id: 3B699956-F248-11E8-B48F-1D18A9856A87
last_name: Ibsen-Jensen
orcid: 0000-0003-4783-0389
- first_name: Andreas
full_name: Pavlogiannis, Andreas
id: 49704004-F248-11E8-B48F-1D18A9856A87
last_name: Pavlogiannis
orcid: 0000-0002-8943-0722
citation:
ama: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. Faster algorithms for quantitative
verification in bounded treewidth graphs. Formal Methods in System Design.
2021;57:401-428. doi:10.1007/s10703-021-00373-5
apa: Chatterjee, K., Ibsen-Jensen, R., & Pavlogiannis, A. (2021). Faster algorithms
for quantitative verification in bounded treewidth graphs. Formal Methods in
System Design. Springer. https://doi.org/10.1007/s10703-021-00373-5
chicago: Chatterjee, Krishnendu, Rasmus Ibsen-Jensen, and Andreas Pavlogiannis.
“Faster Algorithms for Quantitative Verification in Bounded Treewidth Graphs.”
Formal Methods in System Design. Springer, 2021. https://doi.org/10.1007/s10703-021-00373-5.
ieee: K. Chatterjee, R. Ibsen-Jensen, and A. Pavlogiannis, “Faster algorithms for
quantitative verification in bounded treewidth graphs,” Formal Methods in System
Design, vol. 57. Springer, pp. 401–428, 2021.
ista: Chatterjee K, Ibsen-Jensen R, Pavlogiannis A. 2021. Faster algorithms for
quantitative verification in bounded treewidth graphs. Formal Methods in System
Design. 57, 401–428.
mla: Chatterjee, Krishnendu, et al. “Faster Algorithms for Quantitative Verification
in Bounded Treewidth Graphs.” Formal Methods in System Design, vol. 57,
Springer, 2021, pp. 401–28, doi:10.1007/s10703-021-00373-5.
short: K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, Formal Methods in System
Design 57 (2021) 401–428.
date_created: 2021-05-16T22:01:47Z
date_published: 2021-09-01T00:00:00Z
date_updated: 2023-10-10T11:13:20Z
day: '01'
department:
- _id: KrCh
doi: 10.1007/s10703-021-00373-5
ec_funded: 1
external_id:
arxiv:
- '1504.07384'
isi:
- '000645490300001'
intvolume: ' 57'
isi: 1
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://arxiv.org/abs/1504.07384
month: '09'
oa: 1
oa_version: Preprint
page: 401-428
project:
- _id: 2584A770-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: P 23499-N23
name: Modern Graph Algorithmic Techniques in Formal Verification
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
call_identifier: FWF
grant_number: S 11407_N23
name: Rigorous Systems Engineering
- _id: 2581B60A-B435-11E9-9278-68D0E5697425
call_identifier: FP7
grant_number: '279307'
name: 'Quantitative Graph Games: Theory and Applications'
- _id: 2587B514-B435-11E9-9278-68D0E5697425
name: Microsoft Research Faculty Fellowship
publication: Formal Methods in System Design
publication_identifier:
eissn:
- 1572-8102
issn:
- 0925-9856
publication_status: published
publisher: Springer
quality_controlled: '1'
scopus_import: '1'
status: public
title: Faster algorithms for quantitative verification in bounded treewidth graphs
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 57
year: '2021'
...
---
_id: '4460'
abstract:
- lang: eng
text: "Symbolic model checking, which enables the automatic verification of large
systems, proceeds by calculating expressions that represent state sets. Traditionally,
symbolic model-checking tools are based on back- ward state traversal; their basic
operation is the function pre, which, given a set of states, returns the set of
all predecessor states. This is because specifiers usually employ formalisms with
future-time modalities, which are naturally evaluated by iterating applications
of pre. It has been shown experimentally that symbolic model checking can perform
significantly better if it is based, instead, on forward state traversal; in this
case, the basic operation is the function post, which, given a set of states,
returns the set of all successor states. This is because forward state traversal
can ensure that only parts of the state space that are reachable from an initial
state and relevant for the satisfaction or violation of the specification are
explored; that is, errors can be detected as soon as possible.\r\nIn this paper,
we investigate which specifications can be checked by symbolic forward state traversal.
We formulate the problems of symbolic backward and forward model checking by means
of two μ-calculi. The pre-μ calculus is based on the pre operation, and the post-μ
calculus is based on the post operation. These two μ-calculi induce query logics,
which augment fixpoint expressions with a boolean emptiness query. Using query
logics, we are able to relate and compare the symbolic backward and forward approaches.
In particular, we prove that all ω-regular (linear-time) specifications can be
expressed as post-μ queries, and therefore checked using symbolic forward state
traversal. On the other hand, we show that there are simple branching-time specifications
that cannot be checked in this way."
acknowledgement: This research was supported in part by the SRC contract 99-TJ-683.003
and the NSF grant CCR-9988172.
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: Orna
full_name: Kupferman, Orna
last_name: Kupferman
- first_name: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
citation:
ama: Henzinger TA, Kupferman O, Qadeer S. From pre-historic to post-modern symbolic
model checking. Formal Methods in System Design. 2003;23(3):303-327. doi:10.1023/A:1026228213080
apa: Henzinger, T. A., Kupferman, O., & Qadeer, S. (2003). From pre-historic
to post-modern symbolic model checking. Formal Methods in System Design.
Springer. https://doi.org/10.1023/A:1026228213080
chicago: Henzinger, Thomas A, Orna Kupferman, and Shaz Qadeer. “From Pre-Historic
to Post-Modern Symbolic Model Checking.” Formal Methods in System Design.
Springer, 2003. https://doi.org/10.1023/A:1026228213080.
ieee: T. A. Henzinger, O. Kupferman, and S. Qadeer, “From pre-historic to post-modern
symbolic model checking,” Formal Methods in System Design, vol. 23, no.
3. Springer, pp. 303–327, 2003.
ista: Henzinger TA, Kupferman O, Qadeer S. 2003. From pre-historic to post-modern
symbolic model checking. Formal Methods in System Design. 23(3), 303–327.
mla: Henzinger, Thomas A., et al. “From Pre-Historic to Post-Modern Symbolic Model
Checking.” Formal Methods in System Design, vol. 23, no. 3, Springer, 2003,
pp. 303–27, doi:10.1023/A:1026228213080.
short: T.A. Henzinger, O. Kupferman, S. Qadeer, Formal Methods in System Design
23 (2003) 303–327.
date_created: 2018-12-11T12:08:58Z
date_published: 2003-06-20T00:00:00Z
date_updated: 2024-01-10T11:50:31Z
day: '20'
doi: 10.1023/A:1026228213080
extern: '1'
intvolume: ' 23'
issue: '3'
language:
- iso: eng
month: '06'
oa_version: None
page: 303 - 327
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '268'
quality_controlled: '1'
scopus_import: '1'
status: public
title: From pre-historic to post-modern symbolic model checking
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 23
year: '2003'
...
---
_id: '4599'
abstract:
- lang: eng
text: 'State-space explosion is a fundamental obstacle in the formal verification
of designs and protocols. Several techniques for combating this problem have emerged
in the past few years, among which two are significant: partial-order reduction
and symbolic state-space search. In asynchronous systems, interleavings of independent
concurrent events are equivalent, and only a representative interleaving needs
to be explored to verify local properties. Partial-order methods exploit this
redundancy and visit only a subset of the reachable states. Symbolic techniques,
on the other hand, capture the transition relation of a system and the set of
reachable states as boolean functions. In many cases, these functions can be represented
compactly using binary decision diagrams (BDDs). Traditionally, the two techniques
have been practiced by two different schools—partial-order methods with enumerative
depth-first search for the analysis of asynchronous network protocols, and symbolic
breadth-first search for the analysis of synchronous hardware designs. We combine
both approaches and develop a method for using partial-order reduction techniques
in symbolic BDD-based invariant checking. We present theoretical results to prove
the correctness of the method, and experimental results to demonstrate its efficacy.'
acknowledgement: Gerard Holzmann provided us with information on SPIN. Ken McMillan
and Doron Peled contributed through discussions. The VIS group at UC Berkeley and
Rajeev Ranjan in particular helped with the experiments.
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Robert
full_name: Brayton, Robert
last_name: Brayton
- 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: Shaz
full_name: Qadeer, Shaz
last_name: Qadeer
- first_name: Sriram
full_name: Rajamani, Sriram
last_name: Rajamani
citation:
ama: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction
in symbolic state-space exploration. Formal Methods in System Design. 2001;18(2):97-116.
doi:10.1023/A:1008767206905
apa: Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (2001).
Partial-order reduction in symbolic state-space exploration. Formal Methods
in System Design. Springer. https://doi.org/10.1023/A:1008767206905
chicago: Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram
Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal
Methods in System Design. Springer, 2001. https://doi.org/10.1023/A:1008767206905.
ieee: R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order
reduction in symbolic state-space exploration,” Formal Methods in System Design,
vol. 18, no. 2. Springer, pp. 97–116, 2001.
ista: Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order
reduction in symbolic state-space exploration. Formal Methods in System Design.
18(2), 97–116.
mla: Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.”
Formal Methods in System Design, vol. 18, no. 2, Springer, 2001, pp. 97–116,
doi:10.1023/A:1008767206905.
short: R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods
in System Design 18 (2001) 97–116.
date_created: 2018-12-11T12:09:41Z
date_published: 2001-03-01T00:00:00Z
date_updated: 2023-05-08T12:22:38Z
day: '01'
doi: 10.1023/A:1008767206905
extern: '1'
intvolume: ' 18'
issue: '2'
language:
- iso: eng
month: '03'
oa_version: None
page: 97 - 116
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '108'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Partial-order reduction in symbolic state-space exploration
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 18
year: '2001'
...
---
_id: '4582'
abstract:
- lang: eng
text: "We present a formal model for concurrent systems. The model represents synchronous
and asynchronous components in a uniform framework that supports compositional
(assume-guarantee) and hierarchical (stepwise-refinement) design and verification.
While synchronous models are based on a notion of atomic computation step, and
asynchronous models remove that notion by introducing stuttering, our model is
based on a flexible notion of what constitutes a computation step: by applying
an abstraction operator to a system, arbitrarily many consecutive steps can be
collapsed into a single step. The abstraction operator, which may turn an asynchronous
system into a synchronous one, allows us to describe systems at various levels
of temporal detail. For describing systems at various levels of spatial detail,
we use a hiding operator that may turn a synchronous system into an asynchronous
one. We illustrate the model with diverse examples from synchronous circuits,
asynchronous shared-memory programs, and synchronous message-passing protocols.\r\n"
acknowledgement: "We thank Albert Benveniste, Bob Kurshan, Ken McMillan, Amir Pnueli,
and the VIS group at UC Berkeley for fruitful discussions. We also thank the anonymous
referees for suggesting improvements. Alur was supported in part by the DARPA/NASA
grant NAG2-1214 and Henzinger was supported in part by the ONR YIP award N00014-95-1-0520,
the\r\nNSF CAREER award CCR-9501708, the NSF grant CCR-9504469, the DARPA/NASA grant
NAG2-1214, and by the SRC contract 97-DC-324.041."
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Alur R, Henzinger TA. Reactive modules. Formal Methods in System Design.
1999;15(1):7-48. doi:10.1023/A:1008739929481
apa: Alur, R., & Henzinger, T. A. (1999). Reactive modules. Formal Methods
in System Design. Springer. https://doi.org/10.1023/A:1008739929481
chicago: Alur, Rajeev, and Thomas A Henzinger. “Reactive Modules.” Formal Methods
in System Design. Springer, 1999. https://doi.org/10.1023/A:1008739929481.
ieee: R. Alur and T. A. Henzinger, “Reactive modules,” Formal Methods in System
Design, vol. 15, no. 1. Springer, pp. 7–48, 1999.
ista: Alur R, Henzinger TA. 1999. Reactive modules. Formal Methods in System Design.
15(1), 7–48.
mla: Alur, Rajeev, and Thomas A. Henzinger. “Reactive Modules.” Formal Methods
in System Design, vol. 15, no. 1, Springer, 1999, pp. 7–48, doi:10.1023/A:1008739929481.
short: R. Alur, T.A. Henzinger, Formal Methods in System Design 15 (1999) 7–48.
date_created: 2018-12-11T12:09:35Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-02T08:45:58Z
day: '01'
doi: 10.1023/A:1008739929481
extern: '1'
intvolume: ' 15'
issue: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 7 - 48
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '125'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Reactive modules
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 15
year: '1999'
...
---
_id: '4607'
abstract:
- lang: eng
text: We present a verification algorithm for duration properties of real-time systems.
While simple real-time properties constrain the total elapsed time between events,
duration properties constrain the accumulated satisfaction time of state predicates.
We formalize the concept of durations by introducing duration measures for timed
automata. A duration measure assigns to each finite run of a timed automaton a
real number —the duration of the run— which may be the accumulated satisfaction
time of a state predicate along the run. Given a timed automaton with a duration
measure, an initial and a final state, and an arithmetic constraint, the duration-bounded
reachability problem asks if there is a run of the automaton from the initial
state to the final state such that the duration of the run satisfies the constraint.
Our main result is an (optimal) PSPACE decision procedure for the duration-bounded
reachability problem.
acknowledgement: "A preliminary version of this paper appeared in the Proceedings
of the Fifth International Conference on Computer-Aided Verification (CAV 93), Springer-Verlag
LNCS 818, pp. 181–193, 1993. We thank Sergio Yovine for a careful reading of the
manuscript. This reaserch was partially supported by the BRA ESPRIT project REACT,
by the ONR YIP\r\naward N00014-95-1-0520, by the NSF CAREER award CCR-9501708, by
the NSF grants CCR-9200794 and CCR-9504469, by the AFOSR contract F49620-93-1-0056,
and by the ARPA grant NAG2-892."
article_processing_charge: No
article_type: original
author:
- first_name: Rajeev
full_name: Alur, Rajeev
last_name: Alur
- first_name: Costas
full_name: Courcoubetis, Costas
last_name: Courcoubetis
- first_name: Thomas A
full_name: Henzinger, Thomas A
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
citation:
ama: Alur R, Courcoubetis C, Henzinger TA. Computing accumulated delays in real-time
systems. Formal Methods in System Design. 1997;11(2):137-156. doi:10.1023/A:1008626013578
apa: Alur, R., Courcoubetis, C., & Henzinger, T. A. (1997). Computing accumulated
delays in real-time systems. Formal Methods in System Design. Springer.
https://doi.org/10.1023/A:1008626013578
chicago: Alur, Rajeev, Costas Courcoubetis, and Thomas A Henzinger. “Computing Accumulated
Delays in Real-Time Systems.” Formal Methods in System Design. Springer,
1997. https://doi.org/10.1023/A:1008626013578.
ieee: R. Alur, C. Courcoubetis, and T. A. Henzinger, “Computing accumulated delays
in real-time systems,” Formal Methods in System Design, vol. 11, no. 2.
Springer, pp. 137–156, 1997.
ista: Alur R, Courcoubetis C, Henzinger TA. 1997. Computing accumulated delays in
real-time systems. Formal Methods in System Design. 11(2), 137–156.
mla: Alur, Rajeev, et al. “Computing Accumulated Delays in Real-Time Systems.” Formal
Methods in System Design, vol. 11, no. 2, Springer, 1997, pp. 137–56, doi:10.1023/A:1008626013578.
short: R. Alur, C. Courcoubetis, T.A. Henzinger, Formal Methods in System Design
11 (1997) 137–156.
date_created: 2018-12-11T12:09:43Z
date_published: 1997-01-01T00:00:00Z
date_updated: 2022-08-16T13:43:41Z
day: '01'
doi: 10.1023/A:1008626013578
extern: '1'
intvolume: ' 11'
issue: '2'
language:
- iso: eng
month: '01'
oa_version: None
page: 137 - 156
publication: Formal Methods in System Design
publication_identifier:
issn:
- 0925-9856
publication_status: published
publisher: Springer
publist_id: '98'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Computing accumulated delays in real-time systems
type: journal_article
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
volume: 11
year: '1997'
...