| [ABE00] | Parosh Aziz Abdulla, Per Bjesse and Niklas Eén. Symbolic Reachability Analysis based on SAT Solvers. In Proceedings of the 6th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'00), LNCS 1785, pages 411-425. Springer-Verlag, 2000. ( BibTeX ) |
| [ADOW05] | Parosh Aziz Abdulla, Johann Deneux, Joël Ouaknine and James Worrell. Decidability and Complexity Results for Timed Automata via Channel Machines. In Proceedings of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), LNCS 3580, pages 1089-1101. Springer-Verlag, 2005. ( BibTeX ) |
| [Abr79] | Karl Abrahamson. Modal Logic of Concurrent Nondeterministic Programs. In Proceedings of the International Symposium Semantics of Concurrent Computation (SCC'79), LNCS 70, pages 21-33. Springer-Verlag, 1979. ( BibTeX ) |
| [AL02] | Luca Aceto and François Laroussinie. Is your Model Checker on Time? Journal of Logic and Algebraic Programming 52-53, pages 3-51, 2002. ( BibTeX ) |
| [AKM03] | Yasmina Adbeddaïm, Abdelkarim Kerbaa and Oded Maler. Task Graph Scheduling Using Timed Automata. In Proceedings of the 17th International Parallel and Distributed Processing Symposium (IPDPS'03), page 237. IEEE Comp. Soc. Press, 2003. ( BibTeX ) |
| [AM02] | Yasmina Adbeddaïm and Oded Maler. Preemptive Job-Shop Scheduling using Stopwatch Automata. In Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), LNCS 2280, pages 113-126. Springer-Verlag, 2002. ( BibTeX ) |
| [AI03] | Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. ACM Transactions on Computational Logic 4(3), pages 296-314, 2003. ( BibTeX ) |
| [AI01] | Micah Adler and Neil Immerman. An n! Lower Bound On Formula Size. In Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 197-206. IEEE Comp. Soc. Press, 2001. ( BibTeX ) |
| [ÅGJ08] | Thomas Ågotnes, Valentin Goranko and Wojciech Jamroga. Strategic Commitment and Release in Logics for Multi-Agent Systems (Extended abstract). Technical Report 08-01, Clausthal University of Technology, Germany, 2008. ( BibTeX ) |
| [ÅGJ07] | Thomas Ågotnes, Valentin Goranko and Wojciech Jamroga. Alternating-time Temporal Logics with Irrevocable Strategies. In Proceedings of the 11th Conference on Theoretical Aspects of Rationality and Knowledge (TARK'07), pages 15-24. 2007. ( BibTeX ) |
| [AKS04] | Manindra Agrawal, Neeraj Kayal and Nitin Saxena. PRIMES is in P. 2004. ( BibTeX ) |
| [AS04] | Robert Airapetyan and Thorsten Schneider. Protecting Applications with Petri Nets. The Code Breaker's Journal 1(1), 2004. ( BibTeX ) |
| [All97a] | Eric Allender. A Clarification Concerning the #L Hierarchy. 1997. ( BibTeX ) |
| [All97b] | Eric Allender. Making Computation Count: Arithmetic Circuits in the Nineties. SIGACT News 28(4), pages 2-15, 1997. ( BibTeX ) |
| [ABO97] | Eric Allender, Robert Beals and Mitsunori Ogihara. The Complexity of Matrix Rank and Feasible Systems of Linear Equations. Technical Report 97-40, Rutgers University, New Jersey, USA, 1997. ( BibTeX ) |
| [ALR98a] | Eric Allender, Michael C. Loui and Kenneth W. Regan. Complexity Classes. In Handbook of Algorithms and Theory of Computation, pages 27.1-27.23. CRC Press, 1998. ( BibTeX ) |
| [ALR98b] | Eric Allender, Michael C. Loui and Kenneth W. Regan. Other Complexity Classes and Measures. In Handbook of Algorithms and Theory of Computation, pages 29.1-29.24. CRC Press, 1998. ( BibTeX ) |
| [ALR98c] | Eric Allender, Michael C. Loui and Kenneth W. Regan. Reducibility and Completeness. In Handbook of Algorithms and Theory of Computation, pages 28.1-28.28. CRC Press, 1998. ( BibTeX ) |
| [AO96] | Eric Allender and Mitsunori Ogihara. Relationships Among PL, #L, and the Determinant. RAIRO - Theoretical Informatics and Applications 30(1), pages 1-21, 1996. ( BibTeX ) |
| [AS89] | Bowen Alpern and Fred B. Schneider. Verifying Temporal Properties without Temporal Logic. ACM Transactions on Programming Languages and Systems 11(1), pages 147-167, 1989. ( BibTeX ) |
| [AGP+99] | Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis and Sergio Yovine. A Framework for Scheduler Synthesis. In Proceedings of the 20th Symposium on Real-Time Systems (RTS'99), pages 154-163. IEEE Comp. Soc. Press, 1999. ( BibTeX ) |
| [AGS00] | Karine Altisen, Gregor Gößler and Joseph Sifakis. A Methodology for the Construction of Scheduled Systems. In Proceedings of the 6th Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'00), LNCS 1926, pages 106-120. Springer-Verlag, 2000. ( BibTeX ) |
| [AT05] | Karine Altisen and Stavros Tripakis. Implementation of Timed Automata: An Issue of Semantics or Modeling? In Proceedings of the 3rd International Conferences on Formal Modelling and Analysis of Timed Systems, (FORMATS'05), LNCS 3829, pages 273-288. Springer-Verlag, 2005. ( BibTeX ) |
| [AT02] | Karine Altisen and Stavros Tripakis. Tools for Controller Synthesis of Timed Systems. In Proceedings of the 2nd Workshop on Real-Time Tools (RT-TOOLS'02). 2002. ( BibTeX ) |
| [ABM04] | Rajeev Alur, Mikhail Bernadsky and Parthasarathy Madhusudan. Optimal Reachability for Weighted Timed Games. In Proceedings of the 31st International Colloquium on Automata, Languages and Programming (ICALP'04), LNCS, pages 122-133. Springer-Verlag, 2004. ( BibTeX ) |
| [ACD93] | Rajeev Alur, Costas Courcoubetis and David L. Dill. Model-Checking in Dense Real-Time. Information and Computation 104(1), pages 2-34, 1993. ( BibTeX ) |
| [ACD+92] | Rajeev Alur, Costas Courcoubetis, David L. Dill, Nicolas Halbwachs and Howard Wong-Toi. An Implementation of three algorithms for timing verification based on automata emptiness. In Proceedings of the 13th Symposium on Real-Time Systems (RTS'92), pages 157-166. IEEE Comp. Soc. Press, 1992. ( BibTeX ) |
| [ACH+95] | Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis and Sergio Yovine. The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138(1), pages 3-34, 1995. ( BibTeX ) |
| [ACH97] | Rajeev Alur, Costas Courcoubetis and Thomas A. Henzinger. Computing Accumulated Delays in Real Time Systems. Formal Methods in System Design 11(2), pages 137-155, 1997. ( BibTeX ) |
| [ACHH93] | Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger and Pei-Hsin Ho. Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. In Hybrid Systems, LNCS 736, pages 209-229. Springer-Verlag, 1993. ( BibTeX ) |
| [AD94] | Rajeev Alur and David L. Dill. A Theory of Timed Automata. Theoretical Computer Science 126(2), pages 183-235, 1994. ( BibTeX ) |
| [AD90] | Rajeev Alur and David L. Dill. Automata For Modeling Real-Time Systems. In Proceedings of the 17th International Colloquium on Automata, Languages and Programming (ICALP'90), LNCS 443, pages 322-335. Springer-Verlag, 1990. ( BibTeX ) |
| [AELP01] | Rajeev Alur, Kousha Etessami, Salvatore La Torre and Doron A. Peled. Parametric Temporal Logic for "Model Measuring". ACM Transactions on Computational Logic 2(3), pages 388-407, 2001. ( BibTeX ) |
| [AFH96] | Rajeev Alur, Tómas Feder and Thomas A. Henzinger. The Benefits of Relaxing Punctuality. Journal of the ACM 43(1), pages 116-146, 1996. ( BibTeX ) |
| [AH94] | Rajeev Alur and Thomas A. Henzinger. A Really Temporal Logic. Journal of the ACM 41(1), pages 181-203, 1994. ( BibTeX ) |
| [AH93] | Rajeev Alur and Thomas A. Henzinger. Real-time Logics: Complexity and Expressiveness. Information and Computation 104(1), pages 35-77, 1993. ( BibTeX ) |
| [AH92a] | Rajeev Alur and Thomas A. Henzinger. Back to the Future: Towards a Theory of Timed Regular Languages. In Proceedings of the 33rd Annual Symposium on Foundations of Computer Science (FOCS'92), pages 177-186. IEEE Comp. Soc. Press, 1992. ( BibTeX ) |
| [AH92b] | Rajeev Alur and Thomas A. Henzinger. Logics and Models of Real Time: A Survey. In Real-Time: Theory in Practice, Proceedings of REX Workshop 1991, LNCS 600, pages 74-106. Springer-Verlag, 1992. ( BibTeX ) |
| [AHH96] | Rajeev Alur, Thomas A. Henzinger and Pei-Hsin Ho. Automatic Symbolic Verification of Embedded Systems. IEEE Transaction on Software Engineering 22(3), pages 181-201, 1996. ( BibTeX ) |
| [AHK02] | Rajeev Alur, Thomas A. Henzinger and Orna Kupferman. Alternating-time Temporal Logic. Journal of the ACM 49(5), pages 672-713, 2002. ( BibTeX ) |
| [AHK98] | Rajeev Alur, Thomas A. Henzinger and Orna Kupferman. Alternating-time Temporal Logic. In Revised Lectures of the 1st International Symposium on Compositionality: The Significant Difference (COMPOS'97), LNCS 1536, pages 23-60. Springer-Verlag, 1998. ( BibTeX ) |
| [AHK97] | Rajeev Alur, Thomas A. Henzinger and Orna Kupferman. Alternating-time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS'97), pages 100-109. IEEE Comp. Soc. Press, 1997. ( BibTeX ) |
| [AHKV98] | Rajeev Alur, Thomas A. Henzinger, Orna Kupferman and Moshe Y. Vardi. Alternating Refinement Relations. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98), LNCS 1466, pages 163-178. Springer-Verlag, 1998. ( BibTeX ) |
| [AHM+98] | Rajeev Alur, Thomas A. Henzinger, Freddy Y. C. Mang, Shaz Qadeer, Sriram Rajamani and Serdar Tasiran. MOCHA: Modularity in Model Checking. In Proceedings of the 10th International Conference on Computer Aided Verification (CAV'98), LNCS 1427, pages 521-525. Springer-Verlag, 1998. ( BibTeX ) |
| [AHV93] | Rajeev Alur, Thomas A. Henzinger and Moshe Y. Vardi. Parametric Real-Time Reasoning. In Proceedings of the 25th Annual ACM Symposium on the Theory of Computing (STOC'93), pages 592-601. ACM Press, 1993. ( BibTeX ) |
| [AIKY95] | Rajeev Alur, Alon Itai, Robert P. Kurshan and Mihalis Yannakakis. Timing Verification by Successive Approximation. Information and Computation 118(1), pages 142-157, 1995. ( BibTeX ) |
| [AKV98] | Rajeev Alur, Robert P. Kurshan and Mahesh Viswanathan. Membership Question for Timed and Hybrid Automata. In Proceedings of the 19th Symposium on Real-Time Systems (RTS'98), pages 254-263. IEEE Comp. Soc. Press, 1998. ( BibTeX ) |
| [AL04] | Rajeev Alur and Salvatore La Torre. Deterministic Generators and Games for LTL Fragments. ACM Transactions on Computational Logic 5(1), pages 297-322, 2004. ( BibTeX ) |
| [ALM05] | Rajeev Alur, Salvatore La Torre and Parthasarathy Madhusudan. Perturbed Timed Automata. In Proceedings of the 8th International Workshop on Hybrid Systems: Computation and Control (HSCC'05), LNCS 3414, pages 70-85. Springer-Verlag, 2005. ( BibTeX ) |
| [ALM03] | Rajeev Alur, Salvatore La Torre and Parthasarathy Madhusudan. Playing Games with Boxes and Diamonds. In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), LNCS 2761, pages 127-141. Springer-Verlag, 2003. ( BibTeX ) |
| [ALP04] | Rajeev Alur, Salvatore La Torre and George J. Pappas. Optimal paths in weighted timed automata. Theoretical Computer Science 318(3), pages 297-322, 2004. ( BibTeX ) |
| [ALP01] | Rajeev Alur, Salvatore La Torre and George J. Pappas. Optimal paths in weighted timed automata. In Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), LNCS 2034, pages 49-62. Springer-Verlag, 2001. ( BibTeX ) |
| [AM04] | Rajeev Alur and Parthasarathy Madhusudan. Decision Problems for Timed Automata: A Survey. In Formal Methods for the Design of Real-Time Systems - Revised Lectures of the International School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM-RT'04), LNCS 3185, pages 1-24. Springer-Verlag, 2004. ( BibTeX ) |
| [AT96] | Rajeev Alur and Gadi Taubenfeld. Fast Timing-based Algorithms. Distributed Computing 10, pages 1-10, 1996. ( BibTeX ) |
| [ÀG00] | Carme Àlvarez and Raymond Greenlaw. A Compendium of Problems Complete for Symmetric Logarithmic Space. Computational Complexity 9(2), pages 123-145, 2000. ( BibTeX ) |
| [ÀJ95] | Carme Àlvarez and Birgit Jenner. On adaptive DLOGTIME and POLYLOGTIME reductions. Theoretical Computer Science 148(2), pages 183-205, 1995. ( BibTeX ) |
| [ALV01] | Roberto Amadio, Denis Lugiez and Vincent Vanackère. On the Symbolic Reduction of Processes with Cryptographic Functions. Technical Report 4147, INRIA, 2001. ( BibTeX ) |
| [ABF94] | Amihood Amir, Gary Benson and Martin Farach. Let Sleeping Files Lie: Pattern Matching in Z-Comporessed Files. In Proceedings of the 5th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA'94), pages 705-714. ACM Press, 1994. ( BibTeX ) |
| [AH02] | Henrik Reif Andersen and Henrik Hulgaard. Boolean Expression Diagrams. Information and Computation 179(2), pages 194-212, 2002. ( BibTeX ) |
| [Ang80] | Dana Angluin. On Counting Problems and the Polynomial Hierarchy. Theoretical Computer Science 12, pages 161-173, 1980. ( BibTeX ) |
| [AAB00] | Aurore Annichini, Eugene Asarin and Ahmed Bouajjani. Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), LNCS 1855, pages 419-434. Springer-Verlag, 2000. ( BibTeX ) |
| [App02] | Andrew W. Appel. Deobfuscation is in NP. 2002. ( BibTeX ) |
| [AB01] | Carlos Areces and Patrick Blackburn. Bringing them all Together. Journal of Logic and Computation 11(5), pages 657-669, 2001. ( BibTeX ) |
| [ABM00] | Carlos Areces, Patrick Blackburn and Maarten Marx. The Computational Complexity of Hybrid Temporal Logics. Logic Journal of the IGPL 8(5), pages 653-679, 2000. ( BibTeX ) |
| [ABM99] | Carlos Areces, Patrick Blackburn and Maarten Marx. A Road-Map on Complexity for Hybrid Logics. In Proceedings of the 13th International Workshop on Computer Science Logic (CSL'99), LNCS 1862, pages 307-321. Springer-Verlag, 1999. ( BibTeX ) |
| [ABKV03] | Roy Armoni, Doron Bustan, Orna Kupferman and Moshe Y. Vardi. Resets vs. Aborts in Linear Temporal Logic. In Proceedings of the 9th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'03), LNCS 2619, pages 65-80. Springer-Verlag, 2003. ( BibTeX ) |
| [AFF+02] | Roy Armoni, Limor Fix, Alon Flaisher, Rob Gerth, Boris Ginsburg, Tomer Kanza, Avner Landver, Sela Mador-Haim, Eli Singerman, Andreas Tiemeyer, Moshe Y. Vardi and Yael Zbar. The ForSpec Temporal Logic: A New Temporal Property-Specification Language. In Proceedings of the 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), LNCS 2280, pages 296-311. Springer-Verlag, 2002. ( BibTeX ) |
| [AD89] | André Arnold and Anne Dicky. An Algebraic Characterization of Transition System Equivalences. Information and Computation 82(2), pages 198-229, 1989. ( BibTeX ) |
| [AN01] | André Arnold and Damian Niwinski. Complete lattices and fixed-point theorems. In Rudiments of μ-calculus, Studies in Logic and the Foundations of Mathematics 146, chapter 1, pages 1-39. North-Holland, 2001. ( BibTeX ) |
| [AVW03] | André Arnold, Aymeric Vincent and Igor Walukiewicz. Games for Synthesis of Controllers with Partial Observation. Theoretical Computer Science 303(1), pages 7-34, 2003. ( BibTeX ) |
| [ACM97] | Eugene Asarin, Paul Caspi and Oded Maler. A Kleene Theorem for Timed Automata. In Proceedings of the 12th Annual Symposium on Logic in Computer Science (LICS'97), pages 160-171. IEEE Comp. Soc. Press, 1997. ( BibTeX ) |
| [AMP98] | Eugene Asarin, Oded Maler and Amir Pnueli. On Discretization of Delays in Timed Automata and Digital Circuits. In Proceedings of the 9th International Conference on Concurrency Theory (CONCUR'98), LNCS 1466, pages 470-484. Springer-Verlag, 1998. ( BibTeX ) |
| [AMP96] | Eugene Asarin, Oded Maler and Amir Pnueli. Symbolic controller Synthesis for Discrete and Timed Systems. In Hybrid Systems III: Verification and Control, LNCS 1066, pages 1-20. Springer-Verlag, 1996. ( BibTeX ) |
| [AMP95] | Eugene Asarin, Oded Maler and Amir Pnueli. Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives. Theoretical Computer Science 138(1), pages 35-65, 1995. ( BibTeX ) |
| [AMPS98] | Eugene Asarin, Oded Maler, Amir Pnueli and Joseph Sifakis. Controller Synthesis for Timed Automata. In Proceedings of the 5th IFAC Cconference on System Structure and Control (SSC'98), pages 469-474. Elsevier Science, 1998. ( BibTeX ) |
| [AS02] | Eugene Asarin and Gerardo Schneider. Widening the Boundary between Decidable and Undecidable Hybrid Systems. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR'02), LNCS 2421, pages 193-208. Springer-Verlag, 2002. ( BibTeX ) |
| [ASY01] | Eugene Asarin, Gerardo Schneider and Sergio Yovine. On the Decidability of the Reachability Problem for Planar Differential Inclusions. In Proceedings of the 4th International Workshop on Hybrid Systems: Computation and Control (HSCC'01), LNCS 2034, pages 89-104. Springer-Verlag, 2001. ( BibTeX ) |
| [APT86] | Bengt Aspvall, Michael F. Plass and Robert Endre Tarjan. Erratum (A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas). Information Processing Letters 14(4), page 195, 1986. ( BibTeX ) |
| [APT79] | Bengt Aspvall, Michael F. Plass and Robert Endre Tarjan. A Linear-Time Algorithm for Testing the Truth of Certain Quantified Boolean Formulas. Information Processing Letters 8(3), pages 121-123, 1979. Erratum as [APT86]. ( BibTeX ) |
| [Ats02] | Albert Atserias. Unsatisfiable Random Formulas are Hard to Certify. In Proceedings of the 17th Annual Symposium on Logic in Computer Science (LICS'02), pages 325-334. IEEE Comp. Soc. Press, 2002. ( BibTeX ) |
| [AC02] | Jean-Pierre Aubin and Francine Catté. Bilateral Fixed-point and Algebraic Properties of Viability Kernels and Capture Basins of Sets. Technical Report 02-10, CeReMaDe, Université Paris 9, Paris, France, 2002. ( BibTeX ) |
| [dAFH+05] | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar and Mariëlle Stoelinga. Model checking discounted temporal properties. Theoretical Computer Science 345(1), pages 139-170, 2005. ( BibTeX ) |
| [dAFH+03] | Luca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar and Mariëlle Stoelinga. The Element of Surprise in Timed Games. In Proceedings of the 14th International Conference on Concurrency Theory (CONCUR'03), LNCS 2761, pages 142-156. Springer-Verlag, 2003. ( BibTeX ) |
| [dAHM01a] | Luca de Alfaro, Thomas A. Henzinger and Rupak Majumdar. From Verification to Control: Dynamic Programs for Omega-Regular Objectives. In Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 279-290. IEEE Comp. Soc. Press, 2001. ( BibTeX ) |
| [dAHM01b] | Luca de Alfaro, Thomas A. Henzinger and Rupak Majumdar. Symbolic Algorithms for Infinite-State Games. In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01), LNCS 2154, pages 536-550. Springer-Verlag, 2001. ( BibTeX ) |
| [dAHM01c] | Luca de Alfaro, Thomas A. Henzinger and Freddy Y. C. Mang. The Control of Synchronous Systems, Part II. In Proceedings of the 12th International Conference on Concurrency Theory (CONCUR'01), LNCS 2154, pages 566-582. Springer-Verlag, 2001. ( BibTeX ) |
| [dAHM00] | Luca de Alfaro, Thomas A. Henzinger and Freddy Y. C. Mang. The Control of Synchronous Systems. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR'00), LNCS 1877, pages 458-473. Springer-Verlag, 2000. ( BibTeX ) |