1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\citeauthoryear{Alur, Courcoubetis, Halbwachs, Henzinger, Ho,
4: Nicollin, Olivero, Sifakis, and Yovine}{Alur
5: et~al\mbox{.}}{1995}]{ACHHHNOSY95}
6: {\sc Alur, R.}, {\sc Courcoubetis, C.}, {\sc Halbwachs, N.}, {\sc Henzinger,
7: T.~A.}, {\sc Ho, P.~H.}, {\sc Nicollin, X.}, {\sc Olivero, A.}, {\sc Sifakis,
8: J.}, {\sc and} {\sc Yovine, S.} 1995.
9: \newblock The algorithmic analysis of hybrid systems.
10: \newblock {\em Theoretical Computer Science\/}~{\em 138,\/}~1 (February),
11: 3--34.
12:
13: \bibitem[\protect\citeauthoryear{Boigelot}{Boigelot}{1998}]{Boi98}
14: {\sc Boigelot, B.} 1998.
15: \newblock Symbolic methods for exploring infinite state spaces.
16: \newblock Ph.D. thesis, Universit\'e de Li\`ege.
17:
18: \bibitem[\protect\citeauthoryear{Boigelot, Bronne, and Rassart}{Boigelot
19: et~al\mbox{.}}{1997}]{BBR97}
20: {\sc Boigelot, B.}, {\sc Bronne, L.}, {\sc and} {\sc Rassart, S.} 1997.
21: \newblock An improved reachability analysis method for strongly linear hybrid
22: systems.
23: \newblock In {\em Proceedings of the 9th International Conference on
24: Computer-Aided Verification}. Lecture Notes in Computer Science, vol. 1254.
25: Springer-Verlag, Haifa, Israel, 167--177.
26:
27: \bibitem[\protect\citeauthoryear{Boigelot, Jodogne, and Wolper}{Boigelot
28: et~al\mbox{.}}{2001}]{BJW01}
29: {\sc Boigelot, B.}, {\sc Jodogne, S.}, {\sc and} {\sc Wolper, P.} 2001.
30: \newblock On the use of weak automata for deciding linear arithmetic with
31: integer and real variables.
32: \newblock In {\em Proc. International Joint Conference on Automated Reasoning
33: (IJCAR)}. Lecture Notes in Computer Science, vol. 2083. Springer-Verlag,
34: Siena, Italy, 611--625.
35:
36: \bibitem[\protect\citeauthoryear{Boigelot and Latour}{Boigelot and
37: Latour}{2001}]{BL01}
38: {\sc Boigelot, B.} {\sc and} {\sc Latour, L.} 2001.
39: \newblock Counting the solutions of {P}resburger equations without enumerating
40: them.
41: \newblock In {\em Proc. International Conference on Implementations and
42: Applications of Automata}. Lecture Notes in Computer Science, vol. 2494.
43: Springer-Verlag, Pretoria, 40--51.
44:
45: \bibitem[\protect\citeauthoryear{Boigelot, Rassart, and Wolper}{Boigelot
46: et~al\mbox{.}}{1998}]{BRW98}
47: {\sc Boigelot, B.}, {\sc Rassart, S.}, {\sc and} {\sc Wolper, P.} 1998.
48: \newblock On the expressiveness of real and integer arithmetic automata.
49: \newblock In {\em Proc. 25th Colloq. on Automata, Programming, and Languages
50: (ICALP)}. Lecture Notes in Computer Science, vol. 1443. Springer-Verlag,
51: Aalborg, 152--163.
52:
53: \bibitem[\protect\citeauthoryear{Boudet and Comon}{Boudet and
54: Comon}{1996}]{BC96}
55: {\sc Boudet, A.} {\sc and} {\sc Comon, H.} 1996.
56: \newblock Diophantine equations, {Presburger} arithmetic and finite automata.
57: \newblock In {\em Proceedings of {CAAP'96}}. Lecture Notes in Computer Science,
58: vol. 1059. Springer-Verlag, Link{\"o}ping, Sweden, 30--43.
59:
60: \bibitem[\protect\citeauthoryear{Bruy{\`e}re, Hansel, Michaux, and
61: Villemaire}{Bruy{\`e}re et~al\mbox{.}}{1994}]{BHMV94}
62: {\sc Bruy{\`e}re, V.}, {\sc Hansel, G.}, {\sc Michaux, C.}, {\sc and} {\sc
63: Villemaire, R.} 1994.
64: \newblock Logic and $p$-recognizable sets of integers.
65: \newblock {\em Bulletin of the Belgian Mathematical Society\/}~{\em 1,\/}~2
66: (March), 191--238.
67:
68: \bibitem[\protect\citeauthoryear{B{\"u}chi}{B{\"u}chi}{1960}]{Buc60}
69: {\sc B{\"u}chi, J.~R.} 1960.
70: \newblock Weak second-order arithmetic and finite automata.
71: \newblock {\em Zeitschrift Math. Logik und Grundlagen der Mathematik\/}~{\em
72: 6}, 66--92.
73:
74: \bibitem[\protect\citeauthoryear{B{\"u}chi}{B{\"u}chi}{1962}]{Buc62}
75: {\sc B{\"u}chi, J.~R.} 1962.
76: \newblock On a decision method in restricted second order arithmetic.
77: \newblock In {\em Proceedings of the International Congress on Logic, Method,
78: and Philosophy of Science}. Stanford University Press, Stanford, CA, USA,
79: 1--12.
80:
81: \bibitem[\protect\citeauthoryear{Chomicki and Imieli{\'n}ski}{Chomicki and
82: Imieli{\'n}ski}{1988}]{CI88}
83: {\sc Chomicki, J.} {\sc and} {\sc Imieli{\'n}ski, T.} 1988.
84: \newblock Temporal deductive databases and infinite objects.
85: \newblock In {\em Proceedings of the Seventh ACM Symposium on Principles of
86: Database Systems}. ACM Press, Austin, Texas, 61--73.
87:
88: \bibitem[\protect\citeauthoryear{Cobham}{Cobham}{1969}]{Cob69}
89: {\sc Cobham, A.} 1969.
90: \newblock On the base-dependence of sets of numbers recognizable by finite
91: automata.
92: \newblock {\em Mathematical Systems Theory\/}~{\em 3}, 186--192.
93:
94: \bibitem[\protect\citeauthoryear{Courcoubetis, Vardi, Wolper, and
95: Yannakakis}{Courcoubetis et~al\mbox{.}}{1990}]{CVWY90}
96: {\sc Courcoubetis, C.}, {\sc Vardi, M.~Y.}, {\sc Wolper, P.}, {\sc and} {\sc
97: Yannakakis, M.} 1990.
98: \newblock Memory efficient algorithms for the verification of temporal
99: properties.
100: \newblock In {\em Proc. 2nd Workshop on Computer Aided Verification}. Lecture
101: Notes in Computer Science, vol. 531. Springer-Verlag, Rutgers, 233--242.
102:
103: \bibitem[\protect\citeauthoryear{Ferrante and Rackoff}{Ferrante and
104: Rackoff}{1979}]{FR79}
105: {\sc Ferrante, J.} {\sc and} {\sc Rackoff, C.~W.} 1979.
106: \newblock {\em The Computational Complexity of Logical Theories}. Lecture Notes
107: in Mathematics, vol. 718.
108: \newblock Springer-Verlag, Berlin-Heidelberg-New York.
109:
110: \bibitem[\protect\citeauthoryear{Holzmann}{Holzmann}{1997}]{Hol97}
111: {\sc Holzmann, G.~J.} 1997.
112: \newblock The model checker {SPIN}.
113: \newblock {\em IEEE Transactions on Software Engineering\/}~{\em 23,\/}~5
114: (May), 279--295.
115: \newblock Special Issue: Formal Methods in Software Practice.
116:
117: \bibitem[\protect\citeauthoryear{Hopcroft}{Hopcroft}{1971}]{Hop71}
118: {\sc Hopcroft, J.~E.} 1971.
119: \newblock An $n \log n$ algorithm for minimizing states in a finite automaton.
120: \newblock {\em Theory of Machines and Computation\/}, 189--196.
121:
122: \bibitem[\protect\citeauthoryear{Kabanza, St\'evenne, and Wolper}{Kabanza
123: et~al\mbox{.}}{1990}]{KSW90}
124: {\sc Kabanza, F.}, {\sc St\'evenne, J.-M.}, {\sc and} {\sc Wolper, P.} 1990.
125: \newblock Handling infinite temporal data.
126: \newblock In {\em Proc. of the 9th ACM Symposium on Principles of Database
127: Systems}. ACM Press, Nashville, Tennessee, 392--403.
128:
129: \bibitem[\protect\citeauthoryear{Klarlund}{Klarlund}{1991}]{Kla91}
130: {\sc Klarlund, N.} 1991.
131: \newblock Progress measures for complementation of $\omega$-automata with
132: applications to temporal logic.
133: \newblock In {\em Proceedings of the 32nd {IEEE} Symposium on Foundations of
134: Computer Science}. IEEE Computer Society Press, San Juan, 358--367.
135:
136: \bibitem[\protect\citeauthoryear{Kupferman and Vardi}{Kupferman and
137: Vardi}{1997}]{KV97}
138: {\sc Kupferman, O.} {\sc and} {\sc Vardi, M.} 1997.
139: \newblock Weak alternating automata are not that weak.
140: \newblock In {\em Proc. 5th Israeli Symposium on Theory of Computing and
141: Systems}. IEEE Computer Society Press, Ramat-Gan, Israel, 147--158.
142:
143: \bibitem[\protect\citeauthoryear{Kupferman, Vardi, and Wolper}{Kupferman
144: et~al\mbox{.}}{2000}]{KVW00}
145: {\sc Kupferman, O.}, {\sc Vardi, M.~Y.}, {\sc and} {\sc Wolper, P.} 2000.
146: \newblock An automata-theoretic approach to branching-time model checking.
147: \newblock {\em Journal of the ACM\/}~{\em 47,\/}~2 (March), 312--360.
148:
149: \bibitem[\protect\citeauthoryear{Landweber}{Landweber}{1969}]{Lan69}
150: {\sc Landweber, L.~H.} 1969.
151: \newblock Decision problems for $\omega$-automata.
152: \newblock {\em Math. System Theory\/}~{\em 3}, 376--384.
153:
154: \bibitem[\protect\citeauthoryear{??}{{LASH}}{}]{Boi99}
155: {LASH}.
156: \newblock The {L}i\`ege {A}utomata-based {S}ymbolic {H}andler ({LASH}).
157: \newblock Available at :\\ {\tt
158: http://www.montefiore.ulg.ac.be/\~{}boigelot/research/lash/}.
159:
160: \bibitem[\protect\citeauthoryear{L{\"o}\-ding}{L{\"o}\-ding}{2001}]{Loe01}
161: {\sc L{\"o}\-ding, C.} 2001.
162: \newblock Efficient minimization of deterministic weak $\omega-$auto\-ma\-ta.
163: \newblock {\em Information Processing Letters\/}~{\em 79,\/}~3, 105--109.
164:
165: \bibitem[\protect\citeauthoryear{Maler and Staiger}{Maler and
166: Staiger}{1997}]{MS97}
167: {\sc Maler, O.} {\sc and} {\sc Staiger, L.} 1997.
168: \newblock On syntactic congruences for $\omega$-languages.
169: \newblock {\em Theoretical Computer Science\/}~{\em 183,\/}~1, 93--112.
170:
171: \bibitem[\protect\citeauthoryear{Miyano and Hayashi}{Miyano and
172: Hayashi}{1984}]{MH84}
173: {\sc Miyano, S.} {\sc and} {\sc Hayashi, T.} 1984.
174: \newblock Alternating finite automata on $\omega$-words.
175: \newblock {\em Theoretical Computer Science\/}~{\em 32}, 321--330.
176:
177: \bibitem[\protect\citeauthoryear{Muller, Saoudi, and Schupp}{Muller
178: et~al\mbox{.}}{1986}]{MSS86}
179: {\sc Muller, D.~E.}, {\sc Saoudi, A.}, {\sc and} {\sc Schupp, P.~E.} 1986.
180: \newblock Alternating automata, the weak monadic theory of the tree and its
181: complexity.
182: \newblock In {\em Proc. 13th Int. Colloquium on Automata, Languages and
183: Programming}. Springer-Verlag, Rennes, 275--283.
184:
185: \bibitem[\protect\citeauthoryear{Rabin}{Rabin}{1969}]{Rab69}
186: {\sc Rabin, M.~O.} 1969.
187: \newblock Decidability of second order theories and automata on infinite trees.
188: \newblock {\em Transaction of the AMS\/}~{\em 141}, 1--35.
189:
190: \bibitem[\protect\citeauthoryear{Safra}{Safra}{1988}]{Saf88}
191: {\sc Safra, S.} 1988.
192: \newblock On the complexity of omega-automata.
193: \newblock In {\em Proceedings of the 29th {IEEE} Symposium on Foundations of
194: Computer Science}. {IEEE} Computer Society Press, White Plains, 319--327.
195:
196: \bibitem[\protect\citeauthoryear{Semenov}{Semenov}{1977}]{Sem77}
197: {\sc Semenov, A.~L.} 1977.
198: \newblock Presburgerness of predicates regular in two number systems.
199: \newblock {\em Siberian Mathematical Journal\/}~{\em 18}, 289--299.
200:
201: \bibitem[\protect\citeauthoryear{Shiple, Kukula, and Ranjan}{Shiple
202: et~al\mbox{.}}{1998}]{SKR98}
203: {\sc Shiple, T.~R.}, {\sc Kukula, J.~H.}, {\sc and} {\sc Ranjan, R.~K.} 1998.
204: \newblock A comparison of {P}resburger engines for {EFSM} reachability.
205: \newblock In {\em Proceedings of the 10th Intl. Conf. on Computer-Aided
206: Verification}. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag,
207: Vancouver, 280--292.
208:
209: \bibitem[\protect\citeauthoryear{Sistla, Vardi, and Wolper}{Sistla
210: et~al\mbox{.}}{1987}]{SVW87}
211: {\sc Sistla, A.~P.}, {\sc Vardi, M.~Y.}, {\sc and} {\sc Wolper, P.} 1987.
212: \newblock The complementation problem for {B\"uchi} automata with applications
213: to temporal logic.
214: \newblock {\em Theoretical Computer Science\/}~{\em 49}, 217--237.
215:
216: \bibitem[\protect\citeauthoryear{Staiger}{Staiger}{1983}]{Stai83}
217: {\sc Staiger, L.} 1983.
218: \newblock Finite-state $\omega$-languages.
219: \newblock {\em Journal of Computer and System Sciences\/}~{\em 27,\/}~3,
220: 434--448.
221:
222: \bibitem[\protect\citeauthoryear{Staiger and Wagner}{Staiger and
223: Wagner}{1974}]{SW74}
224: {\sc Staiger, L.} {\sc and} {\sc Wagner, K.} 1974.
225: \newblock Automatentheoretische und automatenfreie charakterisierungen
226: topologischer klassen regul{\"a}rer folgenmengen.
227: \newblock {\em Elektron. Informationsverarbeitung und Kybernetik EIK\/}~{\em
228: 10}, 379--392.
229:
230: \bibitem[\protect\citeauthoryear{Thomas}{Thomas}{1990}]{Tho90}
231: {\sc Thomas, W.} 1990.
232: \newblock Automata on infinite objects.
233: \newblock In {\em Handbook of Theoretical Computer Science -- Volume~B: Formal
234: Models and Semantics}, {J.~Van~Leeuwen}, Ed. Elsevier, Amsterdam, Chapter~4,
235: 133--191.
236:
237: \bibitem[\protect\citeauthoryear{Vardi and Wolper}{Vardi and
238: Wolper}{1986a}]{VW86b}
239: {\sc Vardi, M.~Y.} {\sc and} {\sc Wolper, P.} 1986a.
240: \newblock An automata-theoretic approach to automatic program verification.
241: \newblock In {\em Proceedings of the First Symposium on Logic in Computer
242: Science}. IEEE Computer Society Press, Cambridge, 322--331.
243:
244: \bibitem[\protect\citeauthoryear{Vardi and Wolper}{Vardi and
245: Wolper}{1986b}]{VW86}
246: {\sc Vardi, M.~Y.} {\sc and} {\sc Wolper, P.} 1986b.
247: \newblock Automata-theoretic techniques for modal logics of programs.
248: \newblock {\em Journal of Computer and System Science\/}~{\em 32,\/}~2 (April),
249: 183--221.
250:
251: \bibitem[\protect\citeauthoryear{Vardi and Wolper}{Vardi and
252: Wolper}{1994}]{VW94}
253: {\sc Vardi, M.~Y.} {\sc and} {\sc Wolper, P.} 1994.
254: \newblock Reasoning about infinite computations.
255: \newblock {\em Information and Computation\/}~{\em 115,\/}~1 (November), 1--37.
256:
257: \bibitem[\protect\citeauthoryear{Weispfenning}{Weispfenning}{1999}]{Wei99}
258: {\sc Weispfenning, V.} 1999.
259: \newblock Mixed real-integer linear quantifier elimination.
260: \newblock In {\em {ISSAC}: Proceedings of the {ACM} {SIGSAM} International
261: Symposium on Symbolic and Algebraic Computation}. ACM Press, Vancouver,
262: 129--136.
263:
264: \bibitem[\protect\citeauthoryear{Wolper and Boigelot}{Wolper and
265: Boigelot}{1995}]{WB95}
266: {\sc Wolper, P.} {\sc and} {\sc Boigelot, B.} 1995.
267: \newblock An automata-theoretic approach to {Presburger} arithmetic
268: constraints.
269: \newblock In {\em Proc. Static Analysis Symposium}. Lecture Notes in Computer
270: Science, vol. 983. Springer-Verlag, Glasgow, 21--32.
271:
272: \bibitem[\protect\citeauthoryear{Wolper and Boigelot}{Wolper and
273: Boigelot}{2000}]{WB00}
274: {\sc Wolper, P.} {\sc and} {\sc Boigelot, B.} 2000.
275: \newblock On the construction of automata from linear arithmetic constraints.
276: \newblock In {\em Proc. 6th International Conference on Tools and Algorithms
277: for the Construction and Analysis of Systems}. Lecture Notes in Computer
278: Science, vol. 1785. Springer-Verlag, Berlin, 1--19.
279:
280: \end{thebibliography}
281: