1: \newcommand{\etalchar}[1]{$^{#1}$}
2: \def\Nst#1{$#1^{st}$}\def\Nnd#1{$#1^{nd}$}\def\Nrd#1{$#1^{rd}$}\def\Nth#1{$#1^%
3: {th}$}
4: \begin{thebibliography}{A{\v C}JYK96}
5:
6: \bibitem[A{\v C}JYK96]{Parosh:Bengt:Karlis:Tsay:general}
7: Parosh~Aziz Abdulla, Karlis {\v C}er{\=a}ns, Bengt Jonsson, and Tsay Yih-Kuen.
8: \newblock General decidability theorems for infinite-state systems.
9: \newblock In {\em Proc.\ LICS' 96 \Nth{11} IEEE Int.\ Symp.\ on Logic in
10: Computer Science}, pages 313--321, 1996.
11:
12: \bibitem[AJ93]{AbJo:lossy}
13: Parosh~Aziz Abdulla and Bengt Jonsson.
14: \newblock Verifying programs with unreliable channels.
15: \newblock In {\em Proc.\ LICS' 93 \Nth{8} IEEE Int.\ Symp.\ on Logic in
16: Computer Science}, pages 160--170, 1993.
17:
18: \bibitem[AJ96]{AbJo:lossy:IC}
19: Parosh~Aziz Abdulla and Bengt Jonsson.
20: \newblock Verifying programs with unreliable channels.
21: \newblock {\em Information and Computation}, 127(2):91--101, 1996.
22:
23: \bibitem[AJ98]{Parosh:Bengt:Timed:Networks}
24: Parosh~Aziz Abdulla and Bengt Jonsson.
25: \newblock Verifying networks of timed processes.
26: \newblock In Bernhard Steffen, editor, {\em Proc.\ {TACAS '98}, \Nth{4} Int.\
27: Conf.\ on Tools and Algorithms for the Construction and Analysis of Systems},
28: volume 1384 of {\em Lecture Notes in Computer Science}, pages 298--312, 1998.
29:
30: \bibitem[AJ01]{Parosh:Bengt:tutorial}
31: Parosh~Aziz Abdulla and Bengt Jonsson.
32: \newblock Ensuring completeness of symbolic verification methods for
33: infinite-state systems.
34: \newblock {\em Theoretical Computer Science}, 256:145--167, 2001.
35:
36: \bibitem[AJ03]{Parosh:Bengt:Timed:Networks:journal}
37: Parosh~Aziz Abdulla and Bengt Jonsson.
38: \newblock Model checking of systems with many identical timed processes.
39: \newblock {\em Theoretical Computer Science}, 290(1):241--264, 2003.
40:
41: \bibitem[BD91]{Berthomieu:Diaz:TPN}
42: B.~Berthomieu and M.~Diaz.
43: \newblock Modeling and verification of time dependent systems using time
44: {Petri} nets.
45: \newblock {\em IEEE Trans.\ on Software Engineering}, 17(3):259--273, 1991.
46:
47: \bibitem[BLP{\etalchar{+}}99]{CDD:basic}
48: Gerd Behrmann, Kim~G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi.
49: \newblock {Efficient Timed Reachability Analysis Using Clock Difference
50: Diagrams}.
51: \newblock In Nicolas Halbwachs and Doron Peled, editors, {\em Proc.\ \Nth{11}
52: Int.\ Conf.\ on Computer Aided Verification}, number 1633 in Lecture Notes in
53: Computer Science, pages 341--353. Springer--Verlag, July 1999.
54:
55: \bibitem[{\v C}er94]{Cerans:relational:automata:ICALP}
56: K.~{\v C}er{\=a}ns.
57: \newblock Deciding properties of integral relational automata.
58: \newblock In Abiteboul and Shamir, editors, {\em Proc.\ ICALP '94, \Nst{21}
59: International Colloquium on Automata, Languages, and Programming}, volume 820
60: of {\em Lecture Notes in Computer Science}, pages 35--46. Springer Verlag,
61: 1994.
62:
63: \bibitem[CES86]{CES:modelchecking}
64: E.M. Clarke, E.A. Emerson, and A.P. Sistla.
65: \newblock Automatic verification of finite-state concurrent systems using
66: temporal logic specification.
67: \newblock {\em ACM Trans.\ on Programming Languages and Systems},
68: 8(2):244--263, April 1986.
69:
70: \bibitem[Del00]{Delzanno:cache}
71: G.~Delzanno.
72: \newblock Automatic verification of cache coherence protocols.
73: \newblock In Emerson and Sistla, editors, {\em Proc.\ \Nth{12} Int.\ Conf.\ on
74: Computer Aided Verification}, volume 1855 of {\em Lecture Notes in Computer
75: Science}, pages 53--68. Springer Verlag, 2000.
76:
77: \bibitem[DEP99]{Delzanno:etal:broadcast:constr}
78: G.~Delzanno, J.~Esparza, and A.~Podelski.
79: \newblock Constraint-based analysis of broadcast protocols.
80: \newblock In {\em Proc. CSL'99}, 1999.
81:
82: \bibitem[dFERA00]{Escrig:etal:TPN}
83: D.~de~Frutos~Escrig, V.~Valero Ruiz, and O.~{Marroqu\'{i}n} Alonso.
84: \newblock Decidability of properties of timed-arc {Petri} nets.
85: \newblock In {\em ICATPN 2000}, volume 1825, pages 187--206, 2000.
86:
87: \bibitem[Dil89]{Dill:DBM}
88: D.L. Dill.
89: \newblock Timing assumptions and verification of finite-state concurrent
90: systems.
91: \newblock In J.~Sifakis, editor, {\em Automatic Verification Methods for
92: Finite-State Systems}, volume 407 of {\em Lecture Notes in Computer Science}.
93: Springer Verlag, 1989.
94:
95: \bibitem[EFM99]{Esparza:Finkel:Mayr:LICS}
96: J.~Esparza, A.~Finkel, and R.~Mayr.
97: \newblock On the verification of broadcast protocols.
98: \newblock In {\em Proc.\ LICS' 99 \Nth{14} IEEE Int.\ Symp.\ on Logic in
99: Computer Science}, 1999.
100:
101: \bibitem[Fin94]{Finkel:completely:specified}
102: A.~Finkel.
103: \newblock Decidability of the termination problem for completely specified
104: protocols.
105: \newblock {\em Distributed Computing}, 7(3), 1994.
106:
107: \bibitem[FS98]{Finkel:Schnoebelen:everywhere}
108: A.~Finkel and Ph. Schnoebelen.
109: \newblock Well-structured transition systems everywhere.
110: \newblock Technical Report LSV-98-4, Ecole Normale Sup{\'e}rieure de {Cachan},
111: April 1998.
112:
113: \bibitem[GMMP91]{GMMP:TPN}
114: C.~Ghezzi, D.~Mandrioli, S.~Morasca, and M.~Pezz{\`e}.
115: \newblock A unified high-level {Petri} net formalism for time-critical systems.
116: \newblock {\em IEEE Trans.\ on Software Engineering}, 17(2):160--172, 1991.
117:
118: \bibitem[GW93]{GoWo:safety}
119: P.~Godefroid and P.~Wolper.
120: \newblock Using partial orders for the efficient verification of deadlock
121: freedom and safety properties.
122: \newblock {\em Formal Methods in System Design}, 2(2):149--164, 1993.
123:
124: \bibitem[Jan99]{Jancar:csd}
125: Petr Jan{\v c}ar.
126: \newblock {$\omega^2$}-well quasi-orderings and reachability analysis.
127: \newblock Technical Report 158, Department of Computing Systems, {Uppsala
128: University}, 1999.
129:
130: \bibitem[LPY95]{lpw:fct95}
131: Kim~G.\ Larsen, Paul Pettersson, and Wang Yi.
132: \newblock {Model-Checking for Real-Time Systems}.
133: \newblock In {\em Proc.\ of Fundamentals of Computation Theory}, number 965 in
134: Lecture Notes in Computer Science, pages 62--88, August 1995.
135:
136: \bibitem[LPY97]{Uppaal:nutshell}
137: K.G. Larsen, P.~Pettersson, and W.~Yi.
138: \newblock {UPPAAL} in a nutshell.
139: \newblock {\em Software Tools for Technology Transfer}, 1(1-2), 1997.
140:
141: \bibitem[Mar99]{Marcone:entail:bqo}
142: A.~Marcone.
143: \newblock Fine and axiomatic analysis of the quasi-orderings on $\mathcal{P}
144: (q)$.
145: \newblock Technical Report 17/99/RR, {\em Rapporto di Ricerca del Dipartimento
146: di Matematica e Informatica dell'Universit\`a di Udine\/}, 1999.
147:
148: \bibitem[Mil85]{Milner:BQO}
149: E.~C. Milner.
150: \newblock Basic wqo- and bqo-theory.
151: \newblock In I.~Rival, editor, {\em Graphs and Orders}, pages 487--502. {D.
152: Reidel} Publishing Company, 1985.
153:
154: \bibitem[ML98]{DDD:impl}
155: Jesper M{\o}ller and Jakob Lichtenberg.
156: \newblock Dif\-feren\-ce decision dia\-grams.
157: \newblock Master's thesis, Department of Information Technology, Technical
158: University of Denmark, Building 344, DK-2800 Lyngby, Denmark, August 1998.
159:
160: \bibitem[MLAH99]{DDD:basic}
161: Jesper M{\o}ller, Jakob Lichtenberg, Henrik~R. Andersen, and Henrik Hulgaard.
162: \newblock Difference decision diagrams.
163: \newblock Technical Report IT-TR-1999-023, Department of Information
164: Technology, Technical University of Denmark, February 1999.
165:
166: \bibitem[Pou85]{Pouzet:BQO}
167: M.~Pouzet.
168: \newblock Applications of well quasi-orderings and better quasi-orderings.
169: \newblock In I.~Rival, editor, {\em Graphs and Orders}, pages 503--519. {D.
170: Reidel} Publishing Company, 1985.
171:
172: \bibitem[QS82]{QuSi:cesar}
173: J.P. Queille and J.~Sifakis.
174: \newblock Specification and verification of concurrent systems in cesar.
175: \newblock In {\em 5th International Symposium on Programming, Turin}, volume
176: 137 of {\em Lecture Notes in Computer Science}, pages 337--352. Springer
177: Verlag, 1982.
178:
179: \bibitem[RFC99]{PCVC99:TPN:Nondecidability}
180: V.~Valero Ruiz, D.~De Frutos, and F.~Cuartero.
181: \newblock {On Non-Decidability of reachability for Time Arcs Petri Nets}.
182: \newblock In {\em Proceedings . of XXth PNPM}. IEEE. Computer Society, 1999.
183:
184: \bibitem[RP85]{Razouk:Phelps:TPN}
185: R.~Razouk and C.~Phelps.
186: \newblock Performance analysis using timed {Petri} nets.
187: \newblock In {\em Protocol Testing, Specification, and Verification}, pages
188: 561--576, 1985.
189:
190: \bibitem[SBM92]{ScBlMa:outlines}
191: F.~B. Schneider, B.~Bloom, and K.~Marzullo.
192: \newblock Putting time into proof outlines.
193: \newblock In {de Bakker}, Huizing, {de Roever}, and Rozenberg, editors, {\em
194: Real-Time: Theory in Practice}, volume 600 of {\em Lecture Notes in Computer
195: Science}, 1992.
196:
197: \bibitem[VW86]{VW:modelchecking}
198: M.~Y. Vardi and P.~Wolper.
199: \newblock An automata-theoretic approach to automatic program verification.
200: \newblock In {\em Proc.\ LICS '86, \Nst{1} IEEE Int.\ Symp.\ on Logic in
201: Computer Science}, pages 332--344, June 1986.
202:
203: \bibitem[Yov97]{Yovine:kronos}
204: S.~Yovine.
205: \newblock Kronos: A verification tool for real-time systems.
206: \newblock {\em Journal of Software Tools for Technology Transfer}, 1(1-2),
207: 1997.
208:
209: \end{thebibliography}
210: