On the Existence of Network Invariants for Verifying Parameterized Systems? - Correct System Design: Recent Insights and Advances - page 188

merely repeated earlier results. For network invariants, we have presented a result
that guarantees the existence of a network invariant, provided that there is a
simple computational invariant.

We should point out that our results are only partial, and we believe that they
can be made stronger. As they are, they indicate that simple network invariants
exists whenever simple computational invariants exist. The results also show
that the construction of both simple network and computational invariants can
be automated for nite-state systems with only bounded synchronization.

References

ABJ98. Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson. On-the-fly
analysis of systems with unbounded, lossy fo channels. In Proc. 10 th Int.
Conf. on Computer Aided Verication , volume 1427 of Lecture Notes in
Computer Science , pages 305{318, 1998.
ABJN99. Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nils-
son. Handling global conditions in parameterized system verication. In
Proc. 11 th Int. Conf. on Computer Aided Verication , 1999.
ACD90. R. Alur, C. Courcoubetis, and D. Dill. Model-checking for real-time sys-
tems. In Proc. 5 th IEEE Int. Symp. on Logic in Computer Science , pages
414{425, Philadelphia, 1990.
ACHH92. R. Alur, C. Courcoubetis, T. Henzinger, and P.-H. Ho. Hybrid automata:
An algorithmic approach to the specication and vericationof hybrid sys-
tems. In Grossman, Nerode, Ravn, and Rischel, editors, Hybrid Systems ,
number 736 in Lecture Notes in Computer Science, pages 209{229, 1992.
A CJYK96. Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, and Tsay Yih-Kuen.
General decidability theorems for innite-state systems. In Proc. 11 th
IEEE Int. Symp. on Logic in Computer Science , pages 313{321, 1996.

AJ93. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with un-

8 th reliable channels. In Proc. IEEE Int. Symp. on Logic in Computer

Science , pages 160{170, 1993.

AJ98. Parosh Aziz Abdulla and Bengt Jonsson. Verifying networks of timed

processes. In Bernhard Steen, editor, Proc. TACAS '98, 7 th Int. Conf.
on Tools and Algorithms for the Construction and Analysis of Systems ,
volume 1384 of Lecture Notes in Computer Science , pages 298{312, 1998.

AK86. K. Apt and D.C. Kozen. Limits for automatic verication of nite-state

concurrent systems. Information Processing Letters , 22:307{309, 1986.

AL92. M. Abadi and L. Lamport. An old-fashioned recipe for real time. In de

Bakker, Huizing, de Roever, and Rozenberg, editors, Real-Time: Theory
in Practice , volume 600 of Lecture Notes in Computer Science , 1992.

H.R. Andersen. Partial model checking (extended abstract). In Proc. 10 th
IEEE Int. Symp. on Logic in Computer Science , pages 398{407. IEEE
Computer Society Press, 1995.

And95.

BGK + 96.

J. Bengtsson, W. O. D. Grioen, K.J. Kristoersen, K.G. Larsen, F. Lars-
son, P. Pettersson, and W. Yi. Verication of an audio protocol with bus
collision using UPPAAL. In R. Alur and T. Henzinger, editors, Proc. 8 th
Int. Conf. on Computer Aided Verication , volume 1102 of Lecture Notes