@PREAMBLE{ "\def\Nst#1{$#1^{st}$}" # "\def\Nnd#1{$#1^{nd}$}" # "\def\Nrd#1{$#1^{rd}$}" # "\def\Nth#1{$#1^{th}$}" } @STRING(PS = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/\\") @Comment{@STRING(Documents = "http://www.docs.uu.se/~leucker/Documents/\\")} @STRING(Documents = "http://www4.in.tum.de/~leucker/Documents/\\") @string{CAV89 = "Proc.\ Workshop on Computer Aided Verification"} @string{CAV90 = "Proc.\ Workshop on Computer Aided Verification"} @string{CAV91 = "Proc.\ Workshop on Computer Aided Verification"} @string{CAV92 = "Proc.\ Workshop on Computer Aided Verification"} @string{CAV93 = "Proc.\ \Nth{5} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV94 = "Proc.\ \Nth{6} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV95 = "Proc.\ \Nth{7} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV96 = "Proc.\ \Nth{8} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV97 = "Proc.\ \Nth{9} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV98 = "Proc.\ \Nth{10} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV99 = "Proc.\ \Nth{11} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV00 = "Proc.\ \Nth{12} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV01 = "Proc.\ \Nth{13} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV02 = "Proc.\ \Nth{14} Int.\ Conf.\ on Computer Aided Verification"} @string{CAV03 = "Proc.\ \Nth{15} Int.\ Conf.\ on Computer Aided Verification"} @string{LNCS = "Lecture Notes in Computer Science"} @InCollection{Kozen-Tiuryn90, key = "Kozen \& Tiuryn", author = "Dexter Kozen and J. Tiuryn", booktitle = "Handbook of Theoretical Computer Science", title = "Logics of Programs", chapter = 14, publisher = "The MIT Press", year = 1990, editor = "J. van Leeuwen", pages = "789--840", volume = "B: Formal Models and Semantics", address = "New York, N.Y.", annote = "Discussion of dynamic logic. 172 references.", keywords = "logic, dynamic logic, PDL, verification", location = "printed copy, book" } @InCollection{Emerson90a, author = "E. A. Emerson", title = "Temporal and Modal Logic", booktitle = "Handbook of Theoretical Computer Science", chapter = 14, editor = "J. van Leeuwen", publisher = "Elsevier Science Publishers B.V.: Amsterdam, The Netherlands", pages = "996--1072", year = 1990, volume = "B: Formal Models and Semantics", address = "New York, N.Y.", annote = "Discussion of temporal logic. 172 references.", keywords = "logic, temporal logic, CTL, verification", location = "printed copy, book" } @TechReport{Winskel-Nielson93, author = "Glynn Winskel and Mogens Nielsen", title = "Models for Concurrency", address = "Aarhus", year = "1993", annote = "This is, we believe, the final version of a chapter for the Handbook of Logic and the Foundations of Computer Science, Vol. IV, Oxford University Press.", institution = "Basic Research in Computer Science (BRICS)", note = "IB-B941066", abstract = "It surveys a range of models for parallel computation to include interleaving models like transition systems, synchronisation trees and languages (often called Hoare traces in this context), and models like Petri nets, asychronous transition systems, event structures, pomsets and Mazurkiewicz traces where concurrency is represented more explicitly by a form of causal independence. The presentation is unified by casting the models in category-theoretic framework. One aim is to use category theory to provide abstract characterisations of constructions like parallel composition valid throughout a range of different models and use adjunctions to provide formal means for translating between different models. A knowledge of basic category theory is assumed, up to an acquaintance with the notion of adjunction.", keywords = "Concurrency, Event structures, Kategorientheorie, Modell, Nebenlaeufigkeit, Nebenlaeufigkeitstheorie, Petri-Netz, Semantics, Semantik, Trace Theory, Transitionssystem", location = "printed copy, http://theory.doc.ic.ac.uk:80/tfm/papers/WinskelG/", URL = "http://theory.doc.ic.ac.uk:80/tfm/papers/WinskelG/", postscript = PS # "winskel__model_CC.ps.gz", } @Unpublished{Fassbender-Maneth96, author = "Heinz Fa{"s}bender and Sebastian Maneth", title = "A Strict Border for the Decidability of {$E$}-Unification for Recursive Functions", note = "submitted to ALP96", OPTcrossref = "", key = "Fassbender \& Maneth", year = "1996", OPTmonth = "", OPTannote = "", keywords = "E-Unification, recursiv functions, undecidability, decidability, equational theory", location = "printed copy" } @Unpublished{Viry96a, author = "Patrick Viry", title = "Rewriting modulo a rewrite system", note = "submitted to ALP96", OPTcrossref = "", OPTkey = "", year = "1996", OPTmonth = "", OPTannote = "", keywords = "rewriting, equational theory, coherent", location = "printed copy" } @Unpublished{Cleary-Smith96, author = "John G. Cleary and Donald A. Smith", title = "Declarative {I/O}, Assignment and Concurrency", note = "submitted to PLILP96", OPTcrossref = "", OPTkey = "", year = "1996", OPTmonth = "", OPTannote = "", keywords = "Starlog, Templog, temporal logic, declarative i/o, assigment, concurrency", abstract = "{Declarative I/O, Assignment and Concurrency}% Traditionally it has been supposed that it is not possible to combine declarative simplicity, in-place update, side-effecting input and output, explicit concurrency, parallel execution, and execution efficiency. Many proposals have been made that sacrifice one or more of these aims in pursuit of the others. It is claimed that all these aims are compatible using existing logic programming technology. A number of recent research efforts to solve combinations of these problems are reviewed. We demonstrate that within a carefully selected temporal logic framework it is possible to solve all these problems. A simple temporal logic language, called Starlog, is described. Its denotational semantics, in the form of a traditional least fix-point construction is sketched. A number of crucial programming examples are given: assignment and database updates; the optimisation of this to in-place update; interactive input and output; and synchronisation via locks. Crucial aspects of the implementation of the language are discussed. The conclusion is drawn that temporal logic, construed correctly, provides a vehicle for a large range of problem domains that have previously been inaccessible to pure logic programmers. The technology to efficiently implement the proposal is generally available from prior work.", location = "printed copy" } @InProceedings{Gupta93, Author = "Gupta, V.", Title = "Concurrent Kripke Structures", Booktitle = "Proceedings of the North American Process Algebra Workshop, Cornell CS-TR-93-1369", Month=Aug, Year = 1993, keywords = "Kripke structure, event Kripke Structure, event structure, true concurrency", abstract = "We consider a class of Kripke Structures in which the atomic propositions are events. This enables us to represent worlds as sets of events and the transition and satisfaction relations of Kripke structures as the subset and membership relations on sets. We use this class, called event Kripke structures, to model concurrency. The obvious semantics for these structures is a true concurrency semantics. We show how several aspects of concurrency can be easily defined, and in addition get distinctions between causality and enabling, and choice and nondeterminism. We define a duality for event Kripke structures, and show how this duality enables us to convert between imperative and declarative views of programs, by treating states and events on the same footing. We provide pictorial representations of both these views, each encoding all the information to convert to the other. We define a process algebra of event Kripke structures, showing how to combine them in the usual ways---parallel composition, sequential composition, choice, interaction and iteration. Various properties of these connectives like associativity and distributivity are proved. We then show that Winskel's event structures can be embedded in the class of event Kripke structures, and define partial synchronous composition, the primary connective for event structures, for event Kripke structures, and show its equivalence to Winskel's definition.", location = "printed copy, http://boole.stanford.edu/abstracts.html", URL = "http://boole.stanford.edu/abstracts.html" } @PhDThesis{Gup94, Author="Vineet Gupta", Title="Chu Spaces: A Model of Concurrency", School="Stanford University", Month=Sep, Year=1994, abstract = "A Chu space is a binary relation between two sets. In this thesis we show that Chu spaces form a non-interleaving model of concurrency which extends event structures while endowing them with an algebraic structure whose natural logic is linear logic. We provide several equivalent definitions of Chu spaces, including two pictorial representations. Chu spaces represent processes as automata or schedules, and Chu duality gives a simple way of converting between schedules and automata. We show that Chu spaces can represent various concurrency concepts like conflict, temporal precedence and internal and external choice, and they distinguish between causing and enabling events. We present a process algebra for Chu spaces including the standard combinators like parallel composition, sequential composition, choice, interaction, restriction, and show that the various operational identities between these hold for Chu spaces. The solution of recursive domain equations is possible for most of these operations, giving us an expressive specification and programming language. We define a history preserving equivalence between Chu spaces, and show that it preserves the causal structure of a process.", location = "printed copy, http://boole.stanford.edu/chuguide.html#gupthes", URL = "http://boole.stanford.edu/chuguide.html#gupthes" } @Article{Gehrke-Huhn96, author = "T. Gehrke and M. Huhn", title = "{ProFun} --- {A} Language for Executable Specifications", journal = "Lecture Notes in Computer Science", volume = "1140", pages = "304--??", year = "1996", coden = "LNCSD9", ISSN = "0302-9743", acknowledgement = ack-nhfb, bibdate = "Sat Dec 21 09:47:26 1996", annote = "a language similar to Erlang, but strong distinction between functional and concurrent parts, bad presented operational semantics, missing denotational semantics", keywords = "executable specifications, language design, integration of concurrent and functioinal programming, formal reasoning", abstract = "We present a new programming language ProFun which is aimed for the specification and prototype implementation of reactive systems. ProFun combines the paradigms of concurrent and functional programming. A formal operational semantics is developed as a basis for verification techniques. We have implemented a ProFun-compiler which uses C++ as its target language.", location = "printed copy", } @InProceedings{Winskel88, author = "G. Winskel", title = "An introduction to event structures", booktitle = "Proceedings of the School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency", editor = "J. W. de Bakker and W.-P. de Roever and G. Rozenberg", year = 1988, month = jun, series = "Lecture Notes in Computer Science", volume = 354, publisher = "Springer", address = "Berlin Heidelberg New York Tokyo", conflocation = "Noordwijkerhout, The Netherlands, May/", pages = "364--397", keywords = "event structures, Petri nets, traces, concurrency, nondeterminism, parallel computation, semantics, communication processes, higher types, lambda calculus", abstract = "Event structures are models of processes as events constrained by relations of consistency and enabling. These notes are intended to introduce the mathematical theory of event structures, show how they are related to Petri nets and Scott domains, and how they can be used to provide semantics to programming languages for parallel processes as well as languages with higher types.", location = "", } @InProceedings{Mazurkiewicz88, author = "A. Mazurkiewicz", title = "Basic notions of trace theory", booktitle = "Proceedings of the School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency", editor = "J. W. de Bakker and W.-P. de Roever and G. Rozenberg", year = "1988", month = jun, volume = 354, series = "Lecture Notes in Computer Science", publisher = "Springer", conflocation = "Noordwijkerhout, The Netherlands, May/", pages = "364--397", annote = "", keywords = "mazurkiewicz traces, concurrency, processes, partial ordering, Petri nets, semantics", abstract = "The concept of traces has been introduced for describing non-sequential behaviour of concurrent systems via its sequential observations. Traces represent concurrent processes in the same way as strings represent sequential ones. The theory of traces can be used as a tool for reasoning about nets and it is hoped that applying this theory one can get a calculus of the concurrent processes analogous to theat available for sequential systems. The following topics will be discussed: algebraic properties of traces, trace models of some concurrency phenomena, fixed-point calculus for finding the behaviour of nets, modularity, and some applications of the presented theory.", location = "info-bib", } @Book{Reisig86, author = "Wolfgang Reisig", title = "Petrinetze", publisher = "Springer", year = "1986", edition = "2", keywords = "concurrency, processes, partial, Petri nets, semantics", location = "info-bib", } @Book{Winskel93, author = "Glynn Winskel", title = "The Formal Semantics of Programming Languages", publisher = "The MIT Press", year = "1993", address = "Cambrige, Massachusetts", keywords = "semantics", location = "lehrstuhl-bib", } @Article{Kozen83, author = "Dexter Kozen", title = "Results on the Propositional Mu-calculus", journal = "Theoretical Computer Science", year = "1983", volume = "27", pages = "333--354", month = dec, keywords = "CCS, propositional mu-calculus, propositional dynamic logic, decuction, logic", location = "printed copy", } @InProceedings{AlurPP95, title = "Model Checking of Causality Properties", author = "Rajeev Alur and Doron Peled and Wojciech Penczek", pages = "90--100", booktitle = "Proceedings of the 10th Annual {IEEE} Symposium on Logic in Computer Science (LICS'95)", year = "1995", month = jun, address = "San Diego, California", organization ="IEEE Computer Society Press", crossrefonly ="1", comment = "IEEE Computer Society Press Order Number PR07050; IEEE Catalog Number 95CH35768; ISBN 0-8186-7050-9; ISSN Number 1043-6871", keywords = "causality structure, model-checking, tableau construction, decuction, logic", location = "printed copy", } @InCollection(Pratt95d, Author= "Pratt, V.R.", Title= "Chu Spaces and their Interpretation as Concurrent Objects", Booktitle="Computer Science Today: Recent Trends and Developments", Series="Lecture Notes in Computer Science", Volume=1000, Pages="392-405", Editor="van Leeuwen, J.", Publisher="Springer", Year="1995") keywords = "chu spaces, concurrency", abstract = "A Chu space is a binary relation =| from a set A to an antiset X defined as a set which transforms via converse functions. Chu spaces admit a great many interpretations by virtue of realizing all small concrete categories and most large ones arising in mathematical and computational practice. Of particular interest for computer science is their interpretation as computational processes, which takes A to be a schedule of events distributed in time, X to be an automaton of states forming an information system in the sense of Scott, and the pairs (a,x) in the =| relation to be the individual transcriptions of the making of history. The traditional homogeneous binary relations of transition on X and precedence on A are recovered as respectively the right and left residuals of the heterogeneous binary relation =| with itself. The natural algebra of Chu spaces is that of linear logic, made a process algebra by the process interpretation.", location = "printed copy, http://boole.stanford.edu/pub/chuconc.ps.gz", URL = "http://boole.stanford.edu/pub/chuconc.ps.gz" } @InProceedings{Glabbeek-Plotkin95, Author= "Van Glabbeek, R. and Plotkin, G.", Title= "Configuration Structures", Booktitle= "Logic in Computer Science", Pages= "199-209", Month= "June", Publisher= "IEEE Computer Society Press", Year= "1995", keywords = "configuration structures, event structures, petri nets, concurrency, semantincs", abstract = "Configuration structures provide a model of concurrency generalising the families of configurations of event structures. They can be considered logically, as classes of propositional models; then sub-classes can be axiomatised by formulae of simple prescribed forms. Several equivalence relations for event structures are generalised to configuration structures, and also to general Petri nets. Every configuration structure is shown to be ST-bisimulation equivalent to a prime event structure with binary conflict; this fails for the tighter history preserving bisimulation. Finally, Petri nets without self-loops under the collective token interpretation are shown behaviourally equivalent to configuration structures, in the sense that there are translations in both directions respecting history preserving bisimulation. This fails for nets with self-loops.", location = "printed copy, http://boole.stanford.edu/pub/conf.ps.gz", URL = "http://boole.stanford.edu/pub/conf.ps.gz" } @Article{Balbo-Donatelli-Franceschinis92, key = "Balbo et al.", author = "G. Balbo and S. Donatelli and G. Franceschinis", title = "Understanding Parallel Program Behavior through Petri Net Models", journal= "Journal of Parallel and Distributed Computing", pages = "171--187", volume = "15", number = "3", month = jul, year = "1992", location = "CMU Engineering \&{} Science Library (??) Thomas Noll", } @Article{pen93ijfcs, author = "W. Penczek", journal = "International Journal of Foundations of Computer Science", pages = "31--67", title = "Temporal Logics for Trace Systems: On Automated Verification", volume = "4", year = "1993", abstract= "An extension of Computation Tree Logic by past modalities interpreted over Mazurkiewicz's trace systems is defined. The logic is shown to be undecidable. The model checking problem is proved to be $NP$-hard and a one exponential time model checking algorithm for the logic is given. Examples of model checking serializability and inevitability are provided.", location = "printed copy, ps-file, s.u.", URL = "ftp://ftp.win.tue.nl/pub/techreports/wojtek/ijfcs93" } @Article{pen88fi, author = "W. Penczek", title = "A Temporal Logic For Event Structures", journal = "Fundamenta Informaticae", year = 1988, volume = "XI (3)", pages = "297-326", location = "printed copy", } @TechReport{Penczek91, author = "Wojciech Penczek", title = "Branching Time and Partial Order in Temporal Logics", institution = "University of Manchester, Computer Science Department", number = "UMCS-91-3-3", month = mar, year = "1991", url = "http://www.cs.man.ac.uk/csonly/cstechrep/Abstracts/UMCS-91-3-3.html mailto:techreports@cs.man.ac.uk", abstract = "The aim of this report is to present existing formal languages of propositional temporal logic with frames based on branching time structures or, more general, partial orders. Branching time and partial order logics do not only differ in their underlying frames, but also in the way the logics are linked to the behaviour of concurrent systems.", location = "printed copy, ps-file" } @InProceedings{Lichtenstein-Pnueli85, author = "{O. Lichtenstein} and {A. Pnueli}", title = "Checking that Finite State Concurrent Programs Satisfy their Linear Specification", booktitle ="Proceedings of the Twelfth Annual {ACM} Symposium on Principles of Programming Languages", year = "1985", pages = "97--107", organization = "ACM", address = "New York", month = jan, key = "LiPn85", keyword = "LTL, temporal logic, model checking", location = "printed copy", } @InProceedings{Emerson-Srinivasan88, author = "E. A. Emerson and J. Srinivasan", title = "Branching time temporal logic", booktitle = "Proceedings of the School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency", editor = "J. W. de Bakker and W.-P. de Roever and G. Rozenberg", year = "1988", month = jun, volume = 354, series = "Lecture Notes in Computer Science", publisher = "Springer", conflocation = "Noordwijkerhout, The Netherlands, May/", pages = "123--172", location = "printed copy", } @TechReport{Milner91a, author = "Robin Milner", institution = "Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, UK", month = oct, number = "{ECS--LFCS--91--180}", title = "The polyadic $\pi$-calculus: a tutorial", year = 1991, note = "{\em {P}roceedings of the {I}nternational {S}ummer {S}chool on {L}ogic and {A}lgebra of {S}pecification}, {M}arktoberdorf, {A}ugust 1991. Reprinted in {\em Logic and Algebra of Specification}, ed. F. L. Bauer, W. Brauer, and H. Schwichtenberg, Springer, 1993", location = "printed copy", URL = "ftp://ftp.cl.cam.ac.uk/users/rm135/ppi.ps.Z" } @InProceedings{Milner91d, author = "Robin Milner and Joachim Parrow and David Walker", editor = "J. C. M. Baeten and J. F. Groote", title = "Modal Logics for Mobile Processes", booktitle = "Proceedings of CONCUR'91", series = "Lecture Notes in Computer Science", volume = 527, pages = "45--60", publisher = "Springer", address = "Amsterdam", month = aug, year = "1991", keywords= "pcalc mobility equivalence concur91 binder", } @Article{Milner93, author = "R. Milner and J. Parrow and D. Walker", title = "Modal logics for mobile processes", journal = "Theoretical Computer Science", volume = "114", year = "1993", pages = "149--171", } @Book{Ihringer93, author = "Th. Ihringer", title = "Allgemeine Algebra", publisher = "Teubner", address = "Stuttgart", year = "1993", edition = "second", keywords = "Algebra, Huelle, Kongruenz, Verband", abstract = "Eine ausfuehrliche Darstellung der grundlegenden Methoden und Begriffe der Allgemeinen Algebra bis hin zu aktuellen Forschungsergebnissen. Lehrbuch mit Aufgaben.", } @Book{Graetzer68, author = "G. Graetzer", title = "Universal Algebra", publisher = "Van Nostrand Reinhold", address = "Princeton", year = "1968", keywords = "Algebra, Homomorphismus, Modelltheorie, Partiell, Unabhaengigkeit", } @Book{Wechler92, author = "W. Wechler", title = "Universal Algebra for Computer Scientists", publisher= "Springer", address = "Berlin", year = "1992", keywords = "Universal Algebra", } @Book{Herrlich-Strecker79, author = "H. Herrlich and G. E. Strecker", title = "Category Theory", publisher = "Heldermann Verlag", address = "Berlin", edition = "second", year = "1979", keywords= "Kategorientheorie", abstract= "Es wird eine ausfuehrliche Einfuehrung in die Kategorientheorie gegeben. Viele Beispiele werden dargestellt. Die Abschnitte des Buches sind wie folgt gegliedert: 1. Introduction 2. Foundations 3. Categories 4. Special morphism and special objects 5. Functors and natural transformations 6. Limits in categories 7. Adjoint situations 8. Set-valued functors 9. Subobjects, quotient objects, and factorizations 10. Reflective subcategories 11. Pointed categories", } @Article{Robinson65, author = "J. A. Robinson", title = "A Machine-Oriented Logic Based on the Resolution Principle", journal = "Journal of the ACM", volume = 12, number = 1, pages = "23--41", month = jan, year = 1965, bibdate = "Sat Nov 19 21:47:12 1994", keywords = "foundations; history; Prolog; resolution; unification" } @article{Baader86, author = {Baader, F.}, title = {The Theory of Idempotent Semigroups is of Unification Type Zero}, journal = {J. Automated Reasoning}, volume = {2}, pages = {283--286}, year = {1986}} @inproceedings{Baader89, author = {Baader, F.}, title = {Characterizations of Unification Type Zero}, booktitle = {Proceedings of the 3rd International Conference on Rewriting Techniques and Applications, {RTA} 89}, year = {1989}, address = {Chapel Hill (USA)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, pages = {2--14}, volume = {355}} @inproceedings{Baader91, author = {Baader, F.}, title = {Unification, Weak Unification, Upper Bound, Lower Bound and Generalization Problems}, booktitle = {Proceedings of the 4th International Conference on Rewriting Techniques and Applications, {RTA} 91}, year = {1991}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, address = {Como (Italy)}, pages = {86--97}, volume = {488}} @techreport{BaaderNutt90, author = {Baader, F. and Nutt, W.}, title = {Adding Homomorphisms to Commutative/Monoidal Theories, or: {H}ow Algebra Can Help in Equational Unification}, institution= {{D}eutsches {F}orschungszentrum f\"ur {K}\"unstliche {I}ntelligenz, Kaiserslautern}, type = {{DFKI} Research Report}, number = {{RR}-90-16}, year = {1990}} @incollection{BaaderSiekmann94, author = {Baader, F. and Siekmann, J.H.}, title = {Unification Theory}, booktitle = {Handbook of Logic in Artificial Intelligence and Logic Programming}, editor = {D.M. Gabbay and C.J. Hogger and J.A. Robinson}, publisher = {Oxford University Press}, address = {Oxford, UK}, year = {1994} } @Article{buettner90, author = "Wolfram B{\"u}ttner and Klaus Estenfeld and Richard Schmid and Hans-Albert Schneider and Erik Tid{\'e}n", title = "Symbolic Constraint Handling Through Unification in Finite Algebras", journal = "Applicable Algebra in Engineering, Communication and Computing", year = 1990, volume = 1, number = 2, pages = "97--119", month = dec } @TechReport{Nutt92, author = "Werner Nutt", title = "Unification in monoidal theories is solving linear equations over semirings", institution="Deutsches Forschungszentrum f{\"u}r K{\"u}nstliche Intelligenz", number = "92-01", month = jan, year = "1992", } @Article{plotkin72, title ="Building-in Equational Theories", author ="Gordon Plotkin", journal ="Machine Intelligence", volume ="7", year ="1972", month =nov, publisher ="Edinburgh University", pages ="73--90", } @InProceedings{Siekmann79, title ="Unification of commutative terms", author ="J. Siekmann", booktitle ="Proceedings of the Conference on Symbolic and Algebraic Manipulation", pages ="531--545", address ="Marseille (France)", year ="1979", month =jun, publisher ="Springer", series ="Lecture Notes in Computer Science", volume ="72", note ="Also internal report SEKI, 1976", } @Misc{CampusShortCourse, key = "PL", title = "Introduction to Perl", howpublished = "WWW", year = 1996, month = "mar", annote = "Learn Perl in Two Hours", location = "printed copy, ps-file", URL = "http://www.phlab.missouri.edu/perl/perlcourse.ps.gz" } @Unpublished{Reichel95p, author = "Horst Reichel", title = "Formale Modelle der Parallelit{\"a}t", note = "Vorlesungsskript", year = 1995, annote = "Skript einer Vorlesung (V2) gehalten an der Uni Dresden", URL = "http://www.inf.tu-dresden.de/TU/Informatik/ThI/scripte/" } @Unpublished{Reichel95l, author = "Horst Reichel", title = "Logik f{\"u}r Informatiker", note = "Vorlesungsskript", year = 1995, annote = "Skript einer Vorlesung (V2) gehalten an der Uni Dresden", URL = "http://www.inf.tu-dresden.de/TU/Informatik/ThI/scripte/" } @InProceedings{lncs529*105, author = "C. Baier and M. E. Majster-Cederbaum", title = "The Consistency of a Noninterleaving and an Interleaving Model for Full {TCSP}", pages = "105--120", ISBN = "3-540-54458-5", editor = "Lothar Budach", booktitle = "Proceedings of Fundamentals of Computation Theory ({FCT}'91)", conflocation = "Gosen, GER", month = sep, confyear = "1991", series = "Lecture Notes in Computer Science", volume = "529", publisher = "Springer", address = "Berlin, Germany", year = "1991", } @Article{LoogenGoltz91, author = "R. Loogen and U. Goltz", year = "1991", month = jan, journal= "Fundamenta Informaticae", volume = "XIV", number = "1", pages = "39--74", title = "Modelling Nondeterministic Concurrent Processes with Event Structures", location = "printed copy" } @InProceedings{HuZhenjian1996, author = "Zhenjiang Hu and Hideya Iwasaki and Masato Takeichi", title = "Deriving Structural Hylomorphisms from Recursive Definitions", year = "1996", address = "Philadelphia, PA.", url = "http://www.ipl.t.u-tokyo.ac.jp/~hu/pub/icfp96.ps.gz", month = may, pages = "73--82", publisher = "ACM Press", scope = "trans", booktitle = "ACM SIGPLAN International Conference on Functional Programming", keywords= "functional, types, data structures, program transformation", location = "printed copy", } @InProceedings{lncs523*124, author = "Erik Meijer and Maarten Fokkinga and Ross Paterson", title = "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire", pages = "124--144", editor = "John Hughes", booktitle = "Proceedings of Functional Programming Languages an Computer Architecture", month = aug, series = "Lecture Notes in Computer Science", volume = "523", publisher = "Springer", address = "Berlin, Germany", year = "1991", keywords= "functional, types, data structures, program transformation", location = "printed copy", } @Article{Malcolm90a, author = "G. R. Malcolm", title = "Data Structures and Program Transformation", journal = "Science of Computer Programming", volume = "14", pages = "255--279", year = "1990", keywords= "functional, types, data structures, program transformation", abstract= "The starting point in this paper is the {"}Bird-Meertens formalism{"}, a mathematical framework for program transformation currently being developed by R. Bird at Oxford and L. Meertens at Amsterdam. The formalism comprises a concise functional notation and a small number of remarkably powerful theorems for proving equalities of functions. The notation is based on a few elementary operations and is so designed that it lends itself well to the construction of elegant, calculational transformations: from the basic operations, one constructs a specification in algorithmic form - there is no separate specification language - and transforms the specification into a more efficient program. A hallmark of the formalism is that much of this transformation process can be conducted as a linear, equational proof that the original specification is extensionally equal to the resulting more efficient version.", location = "printed copy", } @InCollection{JouannaudKirchner91, author = "Jean-Pierre Jouannaud and Claude Kirchner", booktitle = "Computational Logic: Essays in Honor of Alan Robinson", title = "Solving equations in Abstract Algebras: {A} Rule-Based Survey of Unification", year = "1991", publisher = "{MIT}-Press", editor = "Jean-Louis Lassez and Gordon Plotkin", keywords = "unification, old-team", location = "printed copy", } @Article{Nipkow90, author = "Tobias Nipkow", title = "Unification in Primal Algebras, Their Powers and Their Varieties", journal = "Journal of the ACM", volume = "37", number = "4", pages = "742--776", month = oct, year = "1990", coden = "JACOAH", ISSN = "0004-5411", url = "http://www.acm.org/pubs/toc/Abstracts/0004-5411/96569.html", abstract = "This paper examines the unification problem in the class of {\em primal algebras\/} and the varieties they generate. An algebra is called primal if every function on its carrier can be expressed just in terms of the basic operations of the algebra. The two-element Boolean algebra is the simplest nontrivial example: Every truth-function can be realized in terms of the basic connectives, for example, negation and conjunction.\par It is shown that unification in primal algebras is unitary, that is, if an equation has a solution, it has a single most general one. Two unification algorithms, based on equation-solving techniques for Boolean algebras due to Boole and L{\"o}wenheim, are studied in detail. Applications include certain finite Post algebras and matrix rings over finite fields. The former are algebraic models for many-valued logics, the latter cover in particular modular arithmetic.\par Then unification is extended from primal algebras to their direct powers, which leads to unitary unification algorithms covering finite Post algebras, finite, semisimple Artinian rings, and finite, semisimple nonabelian groups.\par Finally the fact that the variety generated by a primal algebra coincides with the class of its subdirect powers is used. This yields unitary unification algorithms for the equational theories of Post algebras and $p$-rings.", keywords = "Algorithms; Boolean algebra; Boolean rings; equational reasoning; Logic; Post algebra; primal algebras; Theory; unification; Verification", subject = "{\bf F.4.1}: Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Mechanical theorem proving. {\bf F.2.2}: Theory of Computation, ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY, Nonnumerical Algorithms and Problems. {\bf I.1.2}: Computing Methodologies, ALGEBRAIC MANIPULATION, Algorithms, Algebraic algorithms. {\bf I.1.1}: Computing Methodologies, ALGEBRAIC MANIPULATION, Expressions and Their Representation, Simplification of expressions.", } @InCollection{Stirling92, author = "{Stirling, C.}", title = "Modal and Temporal Logics", booktitle = "Handbook of Logic in Computer Science", volume = "2 (Background: Computational Structures)", publisher = "Clarendon Press", year = "1992", pages = "477--563", address = "Oxford", } @Article{Baader89:1, author = "F. Baader", title = "{Unification in Commutative Theories}", journal = "{Journal of Symbolic Computation}", year = "1989", volume = "8", number = "5", pages = "479--498", month = nov, } @PhdThesis{Lawvere93, author = "Lawvere, F.W.", title = "Functional Semantics of Algebraic Theories", school = "Columbia University", year = "1963", } @Book{Kolman93, author = "Bernard Kolman", title = "Introductory Linear Algebra with Applications", publisher = "Pren{\-}tice-Hall", address = "Englewood Cliffs, NJ 07632, USA", edition = "Fifth", pages = "xx + 619", year = "1993", ISBN = "0-02-366032-5", LCCN = "QA184.K67 1993", bibdate = "Wed Aug 30 11:46:00 1995", acknowledgement = ack-nhfb, } @techreport{BRICS-RS-96-62, author = "P. S. Thiagarajan and Igor Walukiewicz", title = "An Expressively Complete {L}inear Time {T}emporal {L}ogic for {M}azurkiewicz Traces", institution = "brics", year = 1996, number = "RS-96-62", address = "daimi", month = dec, note = "i+13~pp. appeared at lics12", abstract = "A basic result concerning $LTL$, the propositional temporal logic of linear time, is that it is expressively complete; it is equal in expressive power to the first order theory of sequences. We present here a smooth extension of this result to the class of partial orders known as Mazurkiewicz traces. These partial orders arise in a variety of contexts in concurrency theory and they provide the conceptual basis for many of the partial order reduction methods that have been developed in connection with $LTL$-specifications.\bibpar We show that $LTrL$, our linear time temporal logic, is equal in expressive power to the first order theory of traces when interpreted over (finite and) {\em infinite} traces. This result fills a prominent gap in the existing logical theory of infinite traces. $LTrL$ also provides a syntactic characterisation of the so called trace consistent (robust) $LTL$-specifications. These are specifications expressed as $LTL$ formulas that do not distiguish between different linearizations of the same trace and hence are amenable to partial order reduction methods", postscript= PS # "thiagaranja_walu__Expr_Compl_LTL_for_Mazur_Traces.ps.gz", URL = "http://www.brics.dk/RS/96/62/BRICS-RS-96-62.ps.gz", location = "printed copy", } @InProceedings{ThiagarajanW1997, title = "An Expressively Complete Linear Time Temporal Logic for {Mazurkiewicz} Traces", author = "P. S. Thiagarajan and I. Walukiewicz", pages = "183--194", booktitle = "Proceedings, Twelth Annual {IEEE} Symposium on Logic in Computer Science", year = "1997", month = "29~" # jun # "--2~" # jul, address = "Warsaw, Poland", organization = "IEEE Computer Society Press", references = "\cite{LICS::AlurPP1995} \cite{ICALP::EbingerM1993} \cite{POPL::GabbayPSS1980} \cite{ICALP::GastinP1992} \cite{MFCS::MukundT1996} \cite{MFCS::Peled1996} \cite{CONCUR::PeledWW1996} \cite{FOCS::Pnueli1977} \cite{LICS::Ramanujam1996} \cite{LICS::Thiagarajan1994} \cite{CONCUR::thiagarajan1995}", } @InCollection{Zucker93a, author = "J. Zucker", editor = "P. E. Lauer", title = "Propositional Temporal Logics and Their Use in Model Checking", booktitle = "Functional Programming, Concurrency, Simulation and Automated Reasoning", pages = "108--116", publisher = "Springer", address = "Berlin, DE", year = "1993", keywords = "LNCS parallel", ISBN = "3-540-56883-2", abstract = "For the sake of proving correctness of programs with respect to their specifications, a number of formalisms exist. A traditional one has been proof systems involving Floyd-Hoare correctness formulae. More recently, especially with regard to concurrent programs such as air traffic control systems or operating systems, which are nonterminating and concurrent, and in connection with the desire for automatic verification, other formalisms have been found to be more useful. The author surveys two such types of formalism which have proved to be particularly successful for efficient automatic verification, or 'model checking'. He considers branching time propositional temporal logics, which serves as a good introduction for the more general formalism of the propositional mu -calculus.", note = "Proceedings of International Lecture Series 1991-92, McMaster UniversityLecture Notes in Computer Science 693.", } @InCollection{Zucker93b, author = "J. Zucker", editor = "P. E. Lauer", title = "The Propositional Mu-Calculus and its Use in Model Checking", booktitle = "Functional Programming, Concurrency, Simulation and Automated Reasoning", pages = "117--128", publisher = "Springer", address = "Berlin, DE", year = "1993", keywords = "LNCS parallel", ISBN = "3-540-56883-2", note = "Proceedings of International Lecture Series 1991-92, McMaster UniversityLecture Notes in Computer Science 693.", } @Article{IC::BoudolC1994, title = "Flow Models of Distributed Computations: Three Equivalent Semantics for {CCS}", author = "G{\'e}rard Boudol and Ilaria Castellani", pages = "247--314", journal = "Information and Computation", month = "1~" # nov, year = "1994", volume = "114", number = "2", references = "\cite{JACM::BerryL1979} \cite{JACM::BrookesHR1984} \cite{JACM::CastellaniH1989} \cite{LICS::DeganoNM1988} \cite{LICS::DeganoMM1989}", } @Article{TCS::SassoneNW1996, title = "Models for concurrency: Towards a classification", author = "Vladimiro Sassone and Mogens Nielsen and Glynn Winskel", pages = "297--348", journal = "Theoretical Computer Science", month = "15~" # dec, year = "1996", volume = "170", number = "1--2", references = "\cite{TCS::NielsenPW1981} \cite{MFCS::SassoneNW1993} \cite{TCS::Stark1989} \cite{TCS::Winskel1985}", } @Article{TCS::AmericaB1988, title = "Designing Equivalent Semantic Models for Process Creation", author = "Pierre America and Jaco de Bakker", pages = "109--176", journal = "Theoretical Computer Science", year = "1988", month = sep, volume = "60", number = "2", note = "Fundamental Study", } @Unpublished{MossesPD:tutas, author = "Peter D. Mosses", title = "A Tutorial on Action Semantics", year = "1996", month = mar, note = "50pp. Tutorial notes for FME'94 (Formal Methods Europe, Barcelona, 1994) and FME'96 (Formal Methods Europe, Oxford, 1996)", annote = "Action Semantics is useful for specifying programming languages: documenting design decisions, setting standards for implementations, etc. This framework has unusually good pragmatics, making specifications easily accessible to programmers. Thanks to its inherent modularity, action semantics scales up smoothly to describing practical, industrially-useful languages. In this 1/2-day tutorial, action semantics is explained, illustrated, and compared to other frameworks such as VDM and RAISE.", keywords = "action semantics, brics, compass-bib, compass-pub", available = "ftp://ftp.brics.dk/pub/BRICS/Projects/AS/Papers/Mosses96DRAFT/", URL = "ftp://ftp.brics.dk/pub/BRICS/Projects/AS/Papers/Mosses96DRAFT/", location = "printed copy" } @Article{Penczek:1993:ATL, author = "W. Penczek", title = "Axiomatizations of temporal logics on trace systems", journal = "Lecture Notes in Computer Science", volume = "665", pages = "452--??", year = "1993", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon May 13 11:49:00 MDT 1996", acknowledgement = ack-nhfb, location = "printed copy", } @Article{Penczek:1992:UPT, author = "W. Penczek", title = "On undecidability of propositional temporal logics on trace systems", journal = "Information Processing Letters", volume = "43", number = "3", pages = "147--??", day = "14", month = sep, year = "1992", coden = "IFPLAT", ISSN = "0020-0190", bibdate = "Wed Jan 3 14:24:13 MST 1996", acknowledgement = ack-nhfb, location = "printed copy", postscript = PS # "penczek_undecidability_logic_on_trace.ps.gz", } @InProceedings{PP95, author = "Doron Peled and Wojciech Penczek", title = "Using Asynchronous {B}{\"u}chi Automata for Efficient Model-Checking of Concurrent Systems", booktitle = "Protocol Specification Testing and Verification", publisher = "Chapman \& Hall", pages = "90--100", year = "1995", address = "Warsaw, Poland", location = "printed copy", postscript = PS # "peled_penczek__ABA.ps.gz" } @Article{Ferreira:1995:TST, author = "W. Ferreira and M. Hennessy", title = "Towards a Semantic Theory of {CML} (Extended Abstract)", journal = "Lecture Notes in Computer Science", volume = "969", pages = "454--??", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, location = "printed copy", } @InProceedings{ICFP::FerreiraHJ1996, title = "A Theory of Weak Bisimulation for Core {CML}", author = "William Ferreira and Matthew Hennessy and Alan Jeffrey", pages = "201--212", booktitle = "Proceedings of the 1996 {ACM} {SIGPLAN} International Conference on Functional Programming", month = "24--26 " # may, year = "1996", address = "Philadelphia, Pennsylvania", references = "\cite{ACTAI::BaetenV1992} \cite{TCS::BergstraK1985} \cite{POPL::BerryMT1992} \cite{LICS::Howe1989} \cite{LICS::Jeffrey1995} \cite{IC::MilnerPW1992:1} \cite{IC::MilnerPW1992} \cite{IC::Moggi1991} \cite{IC::Thomsen1995}", location = "printed copy", } @TechReport{Diekert-Metivier96, type = "Technical Report", number = "TR-1996-02", year = "1996", month = mar, pages = "79", author = "Volker Diekert and Yves M\'etivier", series = "Fakult{\"a}tsbericht 1996/02", cr-category = "F.1.1 Models of Computation", cr-category = "F.1.2 Modes of Computation", cr-category = "G.2.1 Combinatorics", notes = "PostScript (706681 Bytes)", bibdate = "May 29, 1996", title = "Partial Commutation and Traces", institution = "Universit{\"a}t Stuttgart, Fakult{\"a}t Informatik, Germany", url = "ftp://ftp.informatik.uni-stuttgart.de/pub/library/ncstrl.ustuttgart_fi/TR-1996-02", language = "English", abstract = "Parallelism and concurrency are fundamental concepts in computer science. Specification and verification of concurrent programs are of first importance. It concerns our daily life whether software written for distributed systems behaves correctly. It is clear that a satisfactory notion of correctness has to be based on a rigorous mathematical model. Several formalisms have been proposed. Among others there are Petri nets, Hoare's and Milner's CSP and CCS, event structures, and branching temporal logics. The mathematical analysis of these models may become complicated, however. Based on the behavior of elementary net systems Mazurkiewicz introduced the concept of partial commutation to the computer science community. The abstract description of a concurrent process is then called a trace, being defined as a congruence class of a word (sequence) modulo identities of the form ab = ba for some pairs of letters. The success of Mazurkiewicz' approach results from the fact that on one hand partial commutation copes with some important phenomena in concurrency and on the other hand it is close to the classical theory of free monoids describing sequential programs. In particular it is possible to transfer the notion of finite sequential state control to the notion of finite asynchronous state control. There is a satisfactory theory of recognizable languages relating finite semigroups, rational operations, asynchronous automata, and logic. This leads to decidability results and various effective operations. The theory of partial commutation and of trace monoids has been developed both by its interpretation as a model for parallel computation and by its mathematical interest in algebra, formal languages, and combinatorics. Since the beginning in combinatorics by Cartier and Foata (1969) and the formulation of trace theory by Mazurkiewicz (1977) the theory has grown in breadth and depth. It led to significant results with interesting applications. The present contribution reflects some important topics including basic properties and infinite traces. Most of the results are from the monograph [34], but we covered also some new material. Each section gives a short bibliographical remark and leads to further references.", postscript = PS # "diekert_metevier__traces.ps.gz", location = "printed copy", } @Article{Buntine:1994:SED, author = "Wray L. Buntine and Hans-J{\"{u}}rgen B{\"{u}}rckert", title = "On Solving Equations and Disequations", journal = "Journal of the ACM", volume = "41", number = "4", pages = "591--629", month = jul, year = "1994", coden = "JACOAH", ISSN = "0004-5411", bibdate = "Thu Oct 20 23:19:12 1994", url = "http://www.acm.org/pubs/toc/Abstracts/0004-5411/179813.html", abstract = "We are interested in the problem of disunification. Solutions to disunification problems are substitutions for the variables of the problem that make the two terms of each equation equal, but leave those of the disequations different. We investigate this in both algebraic and logical contexts where equality is defined by an equational theory and more generally by a definitive clause equality theory E. We show how E-disunification can be reduced to E-unification, that is, solving equations only, and give a disunification algorithm for theories given a unification algorithm. In fact, this result shows that for theories in which the solutions of all unification problems can also be represented finitely. We sketch how disunification can be applied to handle negation in logic programming with equality in a similar style to Colmerauer's logic programming with rational trees, and to represent many solutions to AC-unification problems by a few solutions to ACI-disunification problems.", acknowledgement = ack-nhfb, keywords = "definite clause; E-disunification; E-unification; equational theory; inequations; languages; logic programming; solving equations and disequations; theory", subject = "{\bf F.4.1}: Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Logic programming. {\bf F.4.1}: Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Computational logic.", location = "printed copy", } @InCollection{C90:mit, author = "Hubert Comon", title = "Disunification: {A} Survey", year = "1991", booktitle = "Computational Logic: Essays in Honor of Alan Robinson", editor = "J.-L. Lassez and G. Plotkin", publisher = "MIT Press", address = "Cambridge, MA", location = "printed copy", } @InProceedings{OrgunMehme1994a, author = "Mehmet Ali Orgun and Wanli Ma", booktitle = "Proceedings of ICTL'94: The 1st International Conference on Temporal Logic", title = "An Overview of Temporal and Modal Logic Programming", year = "1994", abstract-url = "ftp://ftp.mpce.mq.edu.au/pub/comp/techreports/940146.orgun.abs", address = "Berlin Heidelberg", url = "ftp://ftp.mpce.mq.edu.au/pub/comp/techreports/940146.orgun.ps", editor = "D M Gabbay and H J Ohlbach", keywords = "Logic Programming, Temporal Logic, Modal Logic", month = jul, pages = "445--479", publisher = "Springer", scope = "Logic Programming, Temporal Logic", postscript= PS # "orgun_ma__temporal_and_modal_logic_programming.ps.gz", } @Article{IC::KupfermanG1996, title = "Branching-Time Temporal Logic and Tree Automata", author = "Orna Kupferman and Orna Grumberg", pages = "62--69", journal = "Information and Computation", month = "25~" # feb, year = "1996", volume = "125", number = "1", references = "\cite{LNCS::BernholtzG1993} \cite{TCS::Pnueli1981} \cite{IC::VardiW1994:1} \cite{JCSS::VardiW1986} \cite{LNCS::JardJ1989} \cite{FMSD::CourcoubetisVWY1992} \cite{TAMS::Rabin1969:1} \cite{LICS::VardiW1986} \cite{TOPLAS::ClarkeES1986} \cite{ICALP::MullerSS1986} \cite{CAV::BernholtzVW1994} \cite{LNCS::WolperG1993} \cite{CAV::EmersonJS1993}", } @InProceedings{GPVW95, author = "Rob Gerth and Doron Peled and Moshe Y. Vardi and Pierre Wolper", title = "Simple On-the-fly Automatic Verification of Linear Temporal Logic", booktitle = "Protocol Specification Testing and Verification", year = "1995", publisher = "Chapman \& Hall", pages = "3--18", address = "Warsaw, Poland", postscript = PS # "gerth_vardi__on_the_fly_LTL.ps.gz", url = "http://www.cs.rice.edu/~vardi/papers/pstv95rj.ps.Z" } @Article{FantechiGnesiPerticaroli93, author = "A. Fantechi and S. Gnesi and V. Perticaroli", title = "An expressive logic for basic process algebra", journal = "Lecture Notes in Computer Science", volume = "711", pages = "453--??", year = "1993", coden = "LNCSD9", ISSN = "0302-9743", } @InProceedings{Stirling95, author = "C. Stirling", title = "Local Model Checking Games", pages = "1--11", ISBN = "3-540-60218-6", editor = "Insup Lee and Scott A. Smolka", booktitle = "Proceedings of the 6th International Conference on Concurrency Theory ({CONCUR}'95)", month = aug, series = "Lecture Notes in Computer Science", volume = "962", publisher = "Springer", address = "Berlin, GER", year = "1995", } @Misc{Stirling96, author = "C. Stirling", title = "Games for bisimulation and model checking", year = "1996", month = jul, note = "Notes for Mathfit Workshop on finite model theory, University of Wales, Swansea, ", postscript = PS # "stirling__mfit.ps.gz", url = "http://www.dcs.ed.ac.uk/home/cps/mfit.ps", siehe_auch = "Stirling95", } @Article{Burkart92, author = "O. Burkart and B. Steffen", title = "Model Checking for Context-Free Processes", journal = "Lecture Notes in Computer Science", volume = "630", pages = "123--??", year = "1992", coden = "LNCSD9", ISSN = "0302-9743", } @InBook{Emerson97, author = "E. A. Emerson", title = "Model checking and the mu-calculus", chapter = "6", crossref = "Immerman-Kolaitis97", abstract = "1. the mu-calculus, 2. temporal logics, 3. expressiveness, 4. model checking", postscript = PS # "emerson__model_mu.ps.gz", location = "printed copy", } @InBook{Fagin97, author = "R. Fagin", title = "Easier ways to win logical games", chapter = "1", crossref = "Immerman-Kolaitis97", postscript = PS # "fagin__easy_win_games.ps.gz", location = "printed copy", } @Unpublished{Immerman-Vardi97a, author = "Neil Immerman and Moshe Y. Vardi", title = "Model Checking and Transitive Closure Logic (extended version)", year = "1997", postscript = PS # "immerman_vardi__tc_logik_extended.ps.gz", location = "printed copy", crossref = "Immerman-Vardi97", note = "unpublished" } @InProceedings{Immerman-Vardi97, author = "Neil Immerman and Moshe Y. Vardi", title = "Model Checking and Transitive Closure Logic", booktitle = "Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97)", year = "1997", postscript = PS # "immerman_vardi__tc_logik.ps.gz", url = "http://www.cs.umass.edu/~immerman/pub/cav.ps", } @InProceedings{BVW94, author = "O.~Bernholtz and M.~Y.~Vardi and P.~Wolper", title = "An Automata--Theoretic Approach to Branching--Time Model Checking", booktitle = "Proceedings of the 6th International Conference on Computer--Aided Verification (CAV'94)", year = "1994", editor = "D.L.~Dill", pages = "142--155", volume = "818", series = "Lecture Notes in Computer Science", publisher = "Springer", } @Unpublished{KVW98, author = "O. Kupferman and M. Y. Vardi and P.~Wolper", title = "An Automata--Theoretic Approach to Branching--Time Model Checking", year = "1998", note = "Full version of CAV'94 paper", URL = "http://www.cs.rice.edu/~vardi/papers/cav94rj.ps.gz", } @Article{SW91, title = "Local model checking in the modal mu--calculus", author = "Colin Stirling and David Walker", pages = "161--177", journal = "Theoretical Computer Science", year = "1991", volume = "89", number = "1", } @InProceedings{EL86, author = "E.A.~Emerson and C.L.~Lei", title = "Efficient Model Checking in Fragments of the Propositional {$\mu$}--Calculus", pages = "267--278", booktitle = "Symposion on Logic in Computer Science", month = jun, publisher = "IEEE Computer Society Press", address = "Washington, D.C., USA", year = "1986", ISBN = "0-8186-0720-3", } @InBook{Emerson96, author = "E. A. Emerson", title = "Automated Temporal Reasoning about Reactive Systems", crossref = "Moller:1996:LNCS", pages = "41--101", } @InBook{HirshfeldMoller96, author = "Y. Hirshfeld and F. Moller", title = "Decidability Results in Automata and Process Theory", pages = "102--??", crossref = "Moller:1996:LNCS", } @InBook{Stirling96a, author = "C. Stirling", title = "Modal and Temporal Logics for Processes", pages = "149--??", crossref = "Moller:1996:LNCS", } @InBook{Vardi96, author = "Moshe Y. Vardi", title = "An Automata-Theoretic Approach to Linear Temporal Logic", pages = "238--266", location = "printed copy", keywords = "LTL, automata, model checking, alternation", crossref = "Moller:1996:LNCS", } @Book{Moller:1996:LNCS, author = "Faron Moller and G. M. (Graham M.) Birtwistle", title = "Logics for concurrency: structure versus automata", volume = "1043", publisher = "Springer", address = "New York, NY, USA", pages = "xi + 266", year = "1996", coden = "LNCSD9", ISBN = "3-540-60915-6", ISSN = "0302-9743", LCCN = "QA76.9.D5 M645 1996", bibdate = "Sat Dec 21 16:06:37 MST 1996", series = "Lecture Notes in Computer Science", acknowledgement = ack-nhfb, annote = "Specification structures and propositions-as-types for concurrency / Samson Abramsky, Simon Gay and Rajagopal Nagarajan - - Automated temporal reasoning about reactive systems / E. Allen Emerson -- Decidability results in automata and process theory / Yoram Hirshfeld and Faron Moller -- Modal and temporal logics for processes / Colin Stirling -- An automata-theoretic approach to linear temporal logic / Moshe Y. Vardi.", keywords = "Electronic data processing --- Distributed processing; Parallel processing (Computer science)", } @Book{Immerman-Kolaitis97, booktitle = "Descriptive Complexity and Finite Models", title = "Descriptive Complexity and Finite Models", publisher = "American Mathematical Society", year = "1997", editor = "Neil Immerman and Phokion G. Kolaitis", volume = "31", series = "DIMACS: Series in Discrete Mathematics and Theoretical Computer Science", ISSN = "1052-1798", ISBN = " 0-8218-0517-7", preface = "We hope that this small volume will suggest directions of synergy and contact for future researchers to build upon, creating connections and making discoveries that will help explain some of the many mysteries of computation.--from the Preface", annote = "248 pp.", abstract = "Finite model theory can be succinctly described as the study of logics on finite structures. It is an area of research existing between mathematical logic and computer science. This area has been developing through continuous interaction with computational complexity, database theory, and combinatorics. The volume presents articles by leading researchers who delivered talks at the {``}Workshop on Finite Models and Descriptive Complexity{''} at Princeton in January 1996 during a DIMACS sponsored Special Year on Logic and Algorithms. Each article is self-contained and provides a valuable introduction to the featured research areas connected with finite model theory. Contents R. Fagin -- Easier ways to win logical games\\ B. Courcelle -- On the expression of graph\\ properties in some fragments of monadic second-order logic\\ H. Straubing -- Finite models, automata, and circuit complexity\\ V. Vianu -- Databases and finite-model theory \\ M. Y. Vardi -- Why is modal logic so robustly decidable? \\ E. A. Emerson -- Model checking and the mu-calculus \\ T. Pitassi -- Algebraic propositional proof systems", } @TechReport{ClWi96, author = "E. M. Clarke and J. M. Wing", title = "Formal Methods: State of the Art and Future Directions", year = "1996", number = "CMU-CS-96-178", month = sep, institution = "Carnegie Mellon University (CMU)", url = "ftp://reports.adm.cs.cmu.edu/usr/anon/1996/CMU-CS-96-178.ps", postscript = PS # "CMU-CS-96-178.ps.gz", } @Article{BrLe80, author = "J.A. Brzozowski and E. Leiss", title = "On Equations for Regular Languages, Finite Automata, and Sequential Networks", journal = "Theoretical Computer Science", year = "1980", volume = "10", pages = "19--35", key = "BrLe80", keyword = "Rewrite omega", } @Article{Chandra:1981:A, author = "Ashok K. Chandra and Dexter C. Kozen and Larry J. Stockmeyer", title = "Alternation", journal = "Journal of the ACM", volume = "28", number = "1", pages = "114--133", month = jan, year = "1981", coden = "JACOAH", ISSN = "0004-5411", bibdate = "Tue Oct 25 22:09:34 1994", acknowledgement = ack-nhfb, keywords = "alternation; complexity", } @Article{BaierM1994, title = "The Connection between an Event Structure Semantics and an Operational Semantics for {TCSP}", author = "Christel Baier and Mila E. Majster-Cederbaum", journal = "Acta Informatica", pages = "81--104", year = "1994", volume = "31", number = "1", location = "printed copy", abstract = "The relation between an operational interleaving semantics for TCSP based on a transition system and a compositional true concurrency semantics based on event structures is studied.", } @MastersThesis{Stornetta95, author = "Anthony L. Stornetta", title = "Implementation of an Efficient Parallel {BDD} Package", school = "University of California, Santa Barbara", year = "1995", abstract = "Large BDD applications are generally limited by a processor's resources, especially physical memory. In large BDD applications, virtual memory is not an attractive solution for conventional depth-first BDD algorithms. Irregular memory access patterns in the algorithm cause thrashing, which severely impairs performance. One solution to overcoming this resource limitation is to utilize the memory of multiple networked workstations. A number of different forms of parallelism can be exploited in depth-first algorithms performed on a distributed BDD. The BDD structure is stored in a distributed hash table and can be accessed simultaneously by multiple processors. An unlimited number of multiple BDD operations may be concurrently issued. In essence, the package can simultaneously execute multiple threads of computation on a distributed BDD. This thesis presents an efficient parallel BDD package for a distributed environment such as a network of workstations (NOW) or a distributed memory parallel computer. The performance of this parallel BDD package is analyzed, and results for various circuit benchmarks are given.", url = "http://bears.ece.ucsb.edu/personnel/astornet/resume/pbdd.html", postscript = PS # "stornetta__parallel_bdd.ps.gz", } @InProceedings{AndersenHulgaard97, author = "Henrik Reif Andersen and Henrik Hulgaard", title = "Boolean Expression Diagrams", booktitle = "Proceedings, Twelfth Annual {IEEE} Symposium on Logic in Computer Science", year = 1997, organization = "IEEE Computer Society Press", address = "Warsaw, Poland", month = "June 29--July 2", pages = "88--98", abstract = "This paper presents a new data structure called Boolean Expresssion Diagrams (BEDs) for representing and manipulating Boolean functions. BEDs are a generalization of Binary Decision Diagrams (BDDs) which can represent any Boolean circuit in linear space and still maintain many of the desirable properties of BDDs. Two algorithms are described for transforming a BED into a reduced ordered BDD. One closely mimics the BDD apply-operator while the other can exploit the structural information of the Boolean expression. The efficacy of the BED representation is demonstrated by verifying that two 16-bit multiplication circuits (c6288 and c6288nr from the ISCAS 85 benchmarks) implement the same Boolean functions. Using BEDs, this verification problem is solved in a few CPU seconds, while using standard BDD techniques this problem is infeasible. BEDs are useful in applications where the end-result as a reduced ordered BDD is small, for example, for tautology checking or for representing the transition relation when performing a fixed-point iteration in symbolic model checking.", url = "http://andrea.it.dtu.dk/~hra/draft96c-abstract.html", postscript = PS # "Andersen_Hulgaard__BED.ps.gz", } @Article{Dsouza:1995:GBM, author = "A. Dsouza and B. Bloom", title = "Generating {BDD} Models for Process Algebra Terms", journal = "Lecture Notes in Computer Science", volume = "939", pages = "16--??", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, URL = "http://www.cs.cornell.edu/Info/People/dsouza/pa2bdd.ps", postscript = PS # "dsouza_bloom__generating_bdd_models.ps.gz" } @TechReport{HuttonGrah1996c, author = "Graham Hutton and Erik Meijer", institution = "University of Nottingham", title = "Monadic Parser Combinators", year = "1996", url = "http://www.cs.nott.ac.uk/Department/Staff/gmh/bib.html#monparsing", keywords = "monads, parsing, combinators", month = dec, number = "NOTTCS-TR-96-4", type = "Technical Report", scope = "appl", postscript = PS # "haskell/hutton_meijer__monadic_parser_combinators.ps.gz " } @Article{Dsouza:1995:EPC, author = "A. Dsouza and B. Bloom", title = "On the Expressive Power of {CCS}", journal = "Lecture Notes in Computer Science", volume = "1026", pages = "309--??", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, URL = "http://www.cs.cornell.edu/Info/People/dsouza/ccs.ps", postscript = PS # "souza_Bloom__Expressive_Power_CCS.ps.gz" } @InProceedings{KingDandLa1995a, author = "D. King and J. Launchbury", booktitle = "Principles of Programming Languages", title = "Structuring Depth First Search Algorithms in {H}askell", year = "1995", abstract-url = "http://www.cse.ogi.edu/~jl/biblio.html", address = "San Francisco", url = "http://www.cse.ogi.edu/~jl/Papers/dfs.ps", scope = "impmonads", postscript = PS # "haskell/dfs.ps.gz" } @Article{Hudak:1989:CEA, author = "Paul Hudak", title = "Conception, Evolution, and Application of Functional Programming Languages", journal = "ACM Computing Surveys", volume = "21", number = "3", pages = "359--411", month = sep, year = "1989", coden = "CMSVAN", ISSN = "0360-0300", bibdate = "Wed Dec 18 07:42:17 MST 1996", url = "http://www.acm.org/pubs/toc/Abstracts/0360-0300/72554.html", abstract = "The foundations of functional programming languages are examined from both historical and technical perspectives. Their evolution is traced through several critical periods: early work on lambda calculus and combinatory calculus, Lisp, Iswim, FP, ML, and modern functional languages such as Miranda and Haskell. The fundamental premises on which the functional programming methodology stands are critically analyzed with respect to philosophical, theoretical, and pragmatic concerns. Particular attention is paid to the main features that characterize modern functional languages: higher-order functions, lazy evaluation, equations and pattern matching, strong static typing and type inference, and data abstraction. In addition, current research areas --- such as parallelism, nondeterminism, input\slash output, and state-oriented computations --- are examined with the goal of predicting the future development and application of functional languages.", acknowledgement = ack-nhfb, affiliation = "Yale Univ", affiliationaddress = "New Haven, CT, USA", annote = "This is the second paper in the special issue which has a section on non-determinism [along with Bal, et al] which begins with a statement which would sound bizarre to non-programmers or those not familiar with the issues of determinacy.", classification = "723", keywords = "Computer Programming Languages; Functional Programming Languages; Data Abstraction; Lambda Calculus, Additional Key Words and Phrases: Data abstraction; ag; APL; Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.3.2 [Programming Languages]: Language classifications - applicative languages; data-flow languages; denotative [declarative] language; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic - lambda calculus and related systems; FL; FP; grecommended91; Haskell; higher-order functions; Hope; Iswim; K.2 [History of Computing]: software General Terms: Languages; KRC; Lambda Calculus; languages; lazy evaluation; Lisp; Miranda; ML; non-procedural languages; referential transparency; SASL; special issue on programming language paradigms; types; very-high-level languages", review = "ACM CR 9006-0486", subject = "{\bf D.1.1}: Software, PROGRAMMING TECHNIQUES, Applicative (Functional) Programming. {\bf F.4.1}: Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Lambda calculus and related systems. {\bf F.1.2}: Theory of Computation, COMPUTATION BY ABSTRACT DEVICES, Modes of Computation, Parallelism and concurrency. {\bf D.3.2}: Software, PROGRAMMING LANGUAGES, Language Classifications, Applicative languages.", } @Article{cleav-1990:tablemodel:journal:725, year = "1990", author = "R. Cleaveland", title = "Tableau-based model checking in the propositional mu-calculus", journal = "Acta Informatica", volume = "27", number = "8", pages = "725--748", abstract = "This paper describes a procedure, based around the construction of tableau proofs, for determining whether finite-state systems enjoy properties formulated in the propositional mu-calculus. It presents a tableau-based proof system for the logic and proves it sound and complete, and it discusses techniques for the efficient construction of proofs that states enjoy properties expressed in the logic. The approach is the basis of an ongoing implementation of a model checker in the Concurrency Workbench, an automated tool for the analysis of concurrent systems. ", URL = "http://www.cs.sunysb.edu/~rance/publications/papers/ai90.ps.gz", postscript = PS # "cleaveland__tablea_based_mc_mu_calculus.ps.gz" } @InProceedings{lncs575*48, author = "R. Cleaveland and B. Steffen", title = "A Linear--Time Model--Checking Algorithm for the Alternation--Free Modal Mu--Calculus.", pages = "48--58", ISBN = "3-540-55179-4", editor = "Kim G. Larsen and Arne Skou", booktitle = "Proceedings of Computer-Aided Verification ({CAV}'91)", month = jul, series = "Lecture Notes in Computer Science", volume = "575", publisher = "Springer", address = "Berlin, Germany", year = "1992", abstract = "We develop a model-checking algorithm for a logic that permits propositions to be defined using greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics. ", URL = "http://www.cs.sunysb.edu/~rance/publications/papers/fmsd93.ps.gz", postscript = PS # "/cleaveland_steffen__linear_time_mc_altfree_mu_calculus.ps.gz", location = "printed copy" } @Article{Bhat1996:ELM, author = "G. Bhat and R. Cleaveland", title = "Efficient Local Model-Checking for Fragments of the Modal mu-Calculus", journal = "Lecture Notes in Computer Science", volume = "1055", pages = "107--??", year = "1996", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, abstract = "This paper develops efficient local model-checking algorithms for expressive fragments of the modal mu-calculus. The time complexity of our procedures matches that of the best existing global algorithms; however, in contrast to those routines, ours explore a system's state space in a need-driven fashion and do not require its a priori construction. Consequently, our algorithms should perform better in practice. Our approach relies on a novel reformulation of the model-checking problem for the modal mu-calculus in terms of checking whether certain linear-time temporal formulas are satisfied by generalized Kripke structures that we call and-or Kripke structures.", URL = "http://www.cs.sunysb.edu/~rance/publications/papers/tacas96a.ps.gz", postscript = PS # "cleaveland/bhat_cleaveland__efficient_local_mc_for_fragments.ps.Z" } @InProceedings{LICS::BhatC1996, title = "Efficient Model Checking via the Equational {$\mu$}-Calculus", author = "Girish Bhat and Rance Cleaveland", pages = "304--312", booktitle = "Proceedings, 11$^{\mathrm{th}}$ Annual {IEEE} Symposium on Logic in Computer Science", year = "1996", month = "27--30 " # jul, address = "New Brunswick, New Jersey", organization = "IEEE Computer Society Press", references = "\cite{LICS::Andersen1995} \cite{LICS::BurchCMDH1990} \cite{TOPLAS::ClarkeES1986} \cite{ACTAI::Cleaveland1989} \cite{LICS::EmersonL1986} \cite{SCP::EmersonL1987} \cite{TCS::Kozen1983} \cite{POPL::LichtensteinP1985} \cite{LICS::VardiW1986}", abstract = "This paper studies the use of an equational variant of the modal mu-calculus as a unified framework for efficient temporal logic model checking. In particular, we show how an expressive temporal logic, CTL*, may be efficiently translated into the mu-calculus. Using this translation, one may then employ mu-calculus model-checking techniques, including on-the-fly procedures, BDD-based algorithms and compositional model-checking approaches, to determine if systems satisfy formulas in CTL*. ", URL = "http://www.cs.sunysb.edu/~rance/publications/papers/lics96a.ps.gz", postscript = PS # "bhat_cleaveland__efficient_mc_via_equational_mu_calculus.ps.Z" } @InProceedings{POPL::ChenH1997, title = "Rolling Your Own Mutable {ADT}---{A} Connection Between Linear Types and Monads", author = "Chih-Ping Chen and Paul Hudak", pages = "54--66", booktitle = "Conference Record of {POPL}'97: The 24th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", month = "15--17 " # jan, year = "1997", address = "Paris, France", references = "\cite{POPL::AriolaFMOW1995} \cite{LICS::GuzmanH1990} \cite{POPL::Launchbury1993} \cite{TCS::Lafont1988} \cite{LICS::Moggi1989} \cite{POPL::OderskyRH1993} \cite{POPL::JonesW1993} \cite{TOPLAS::Schmidt1985} \cite{POPL::Wadler1992}", abstract = "Monadic and CPS approaches to I/O, state, etc. have become quite popular in the pure functional programming community. In an attempt to understand formally why these approaches ``work'' (in the sense of actually achieving the efficiency of ``in-place update'') I have developed a modest theory of mutable abstract datatypes (MADTs), which can be expressed in direct, monadic, or CPS styles. This work was originally described in the paper Mutable Abstract Datatypes --or-- How to Have Your State and Munge It, Too , but a more recent paper will appear in the upcoming POPL Symposium, titled: Rolling Your Own Mutable ADT -- A Connection Between Linear Types and Monads , co-authored with my student Chih-Ping Chen. ", URL = "http://www.cs.yale.edu/homes/hudak-dir/popl97.ps", postscript = PS # "haskell/madt.ps.Z" } @Article{Finne:1996:CUI, author = "S. Finne and S. P. Jones", title = "Composing the User Interface with {Haggis}", journal = "Lecture Notes in Computer Science", volume = "1129", pages = "1--??", year = "1996", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Tue Oct 29 14:12:39 MST 1996", acknowledgement = ack-nhfb, URL = "ftp://ftp.dcs.gla.ac.uk/pub/glasgow-fp/authors/Sigbjorn_Finne/haggis-tutorial.ps.gz", postscript = PS # "haskell/haggis-tutorial.ps.gz", } @Article{Walukiewicz:1997, author = "I. Walukiewicz and D. Niwi\'wski", title = "Games for the $\mu$-calulus", journal = "Theoretical Computer Science", volume = "163", pages = "99--116", year = "1997", URL = "http://zls.mimuw.edu.pl/~igw/games.ps", postscript = PS # "walukiewicz__games_for_the_mu_calculus.ps.gz" } @InProceedings{FinnePeytonJones95, author = "Sigbjorn Finne and Simon Peyton Jones", title = "Composing {H}aggis", key = "FPJ95", booktitle = "Proceedings of the Fifth Eurographics Workshop on Programming Paradigms in Computer Graphics", year = "1995", address = "Maastrict, Netherlands", month = sep, URL = "http://www.dcs.gla.ac.uk/~sof/haggis/composing-haggis.ps.gz", postscript = PS # "haskell/finne_jones__composing_haggis.ps.gz", } @InProceedings{POPL::JonesGF1996, title = "Concurrent {Haskell}", author = "Simon Peyton Jones and Andrew Gordon and Sigbjorn Finne", pages = "295--308", booktitle = "Conference Record of {POPL}'96: The $23^{\mathrm{rd}}$ {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages", month = "21--24 " # jan, year = "1996", address = "St.\ Petersburg Beach, Florida", references = "\cite{LICS::Jeffrey1995}", URL = "http://www.dcs.gla.ac.uk/~sof/haggis/composing-haggis.ps.gz", postscript = PS # "haskell/concurrent-haskell.ps.gz", } @Proceedings{SPIN, editor = "Jean-Charles Gr\'egoire and Gerard J. Holzmann and Doron A. Peled", title = "The Spin Verification System", year = "1997", volume = "32", series = "DIMACS series", publisher = "American Mathematical Society", note = "ISBN 0-8218-0680-7, 203p", } @Manual{Mo92, author = "F. Moller", title = "{The Edinburgh Concurrency Workbench (Version 6.1)}", year = "1992", month = oct, organization = "Department of Computer Science, University of Edinburgh", } @InProceedings{Cleaveland96, author = "R. Cleaveland and S. Sims", title = "The {NCSU} Concurrency Workbench", booktitle = "Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV'96)", series = "Lecture Notes in Computer Science", volume = "1102", pages = "394--397", year = "1996", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Fri Sep 6 19:46:15 MDT 1996", acknowledgement = ack-nhfb, } @InProceedings{Wing-sigsoft95, author = "Jeannette M. Wing and Mandana Vaziri-Farahani", title = "{Model Checking Software Systems: A Case Study}", booktitle = "Proceedings of SIGSOFT'95 Third ACM SIGSOFT Symposium on the Foundations of Software Engineering", pages = "128--139", month = oct, year = "1995", abstract = "Model checking is a proven successful technology for verifying hardware. It works, however, on only finite state machines, and most software systems have infinitely many states. Our approach to applying model checking to software hinges on identifying appropriate abstractions that exploit the nature of both the system, S, and the property, $\phi$, to be verified. We check $\phi$ on an abstracted, but finite, model of S. Following this approach we verified three cache coherence protocols used in distributed file systems. These protocols have to satisfy this property: ``If a client believes that a cached file is valid then the authorized server believes that the client's copy is valid.'' In our finite model of the system, we need only represent the ``beliefs'' that a client and a server have about a cached file; we can abstract from the caches, the files' contents, and even the files themselves. Moreover, by successive application of the generalization rule from predicate logic, we need only consider a model with at most two clients, one server, and one file. We used McMillan's SMV model checker; on our most complicated protocol, SMV took less than 1 second to check over 43,600 reachable states.", } @TechReport{McMi92b, author = "K. L. McMillan", title = "The {SMV} system, Symbolic Model Checking - an approach", institution = "Carnegie Mellon University", year = "1992", number = "CMU-CS-92-131", key = "McMi92b", keyword = "hardware verification general techreport", } @Book{McMi93a, author = "K. L. McMillan", title = "{S}ymbolic {M}odel {C}hecking", publisher = "Kluwer Academic Publishers", year = "1993", address = "Norwell Massachusetts", key = "McMi93a", } @Book{MilCC89, author = "R. Milner", title = "Communication and Concurrency", publisher = "Prentice Hall", year = "1989", series = "International Series in Computer Science", } @InProceedings{Cleaveland95FGV, author = "R. Cleaveland and E. Madelaine and S. Sims", title = "A front-end generator for verification tools", booktitle = "Proc.\ of the Int.\ Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95)", journal = "Lecture Notes in Computer Science", series = "Lecture Notes in Computer Science", volume = "1019", pages = "153--173", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", URL = "http://www.csc.ncsu.edu/eos/users/s/stsims/WWW/papers/pac.ps", postscript = PS # "Cleaveland_Madelaine_Sims__front_end_generator_verifactions_tools.ps.gz", } @InProceedings{Bryant85, author = "R. E. Bryant", title = "Symbolic Manipulation of Boolean Functions Using a Graphical Representation", pages = "688--694", booktitle = "Proceedings of the 22nd {ACM}/{IEEE} Design Automation Conference", ISBN = "0-8186-0635-5", month = jun, publisher = "IEEE Computer Society Press", address = "Los Alamitos, Ca., USA", year = "1985", } @TechReport{CMU//CS-94-204, bibdate = "September 13, 1995", type = "Technical Report", number = "CS-94-204", title = "Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking", year = "1994", month = oct, institution = "Carnegie Mellon University, School of Computer Science", pages = "19", author = "Edmund Clarke and Orna Grumberg and Kenneth McMillan and Xudong Zhao", abstract = "Model checking is an automatic technique for verifying sequential circuit designs and protocols. An efficient search procedure is used to determine whether or not the specification is satisfied. If it is not satisfied, our technique will produce a counterexample execution trace that shows the cause of the problem. Although finding counterexamples is extremely important, there is no description of how to do this in the literature on model checking. We describe an efficient algorithm to produce counterexamples and witnesses for symbolic model checking algorithms. This algorithm is used in the SMV model checker and works quite well in practice. We also discuss how to extend our technique to more complicated specifications. This extension makes it possible to find counterexamples for verification procedures based on showing language containment between various types of @g(w)-automata.", notes = "Automatic verification, temporal logic, model checking, binary decision diagrams, counterexamples", } @InCollection{BaVe94, author = "J. C. M. Baeten and C. Verhoef", title = "Concrete Process Algebra", booktitle = "Handbook of Logic in Computer Science", editor = "S. Abramsky and D. Gabbay and T. S. E. Maibaum", year = "1994", publisher = "Oxford University Press", pages = "149--268", crossref = "HLCS4", } @Book{HLCS1, editor = "Samson Abramsky and Dov M.\ Gabbay and Thomas S.\ E.\ Maibaum", publisher = "Oxford University Press", title = "Handbook of Logic in Computer Science. Background: Mathematical Structures", volume = "1", year = "1992", location = "book", } @Book{HLCS2, editor = "Samson Abramsky and Dov M.\ Gabbay and Thomas S.\ E.\ Maibaum", publisher = "Oxford University Press", title = "Handbook of Logic in Computer Science. Background: Computational Structures", volume = "2", year = "1992", } @Book{HLCS3, editor = "Samson Abramsky and Dov M.\ Gabbay and Thomas S.\ E.\ Maibaum", publisher = "Oxford University Press", title = "Handbook of Logic in Computer Science. Semantic Structures", volume = "3", year = "1994", } @Book{HLCS4, editor = "Samson Abramsky and Dov M.\ Gabbay and Thomas S.\ E.\ Maibaum", publisher = "Oxford University Press", title = "Handbook of Logic in Computer Science. Semantic Modelling", volume = "4", year = "1995", } @InCollection{BolognesiBrinksma89, author = "T. Bolognesi and E. Brinksma", title = "Introduction to the {ISO} specification language {LOTOS}", booktitle = "The Formal Description Technique LOTOS", editor = "P. H. J. van Eijk and C. A. Vissers and M. Diaz", publisher = "Elsevier Science Publishers North-Holland", year = "1989", pages = "23--73", } @Article{Harel87, key = "Harel", author = "David Harel", title = "Statecharts: {A} Visual Formalism for Complex Systems", journal = "Science of Computer Programming", year = "1987", volume = "8", number = "3", month = jun, pages = "231--274", } @InProceedings{BestHop93, author = "Eike Best and Richard P. Hopkins", title = "{B(PN)}$^2$ --- {A} Basic {P}etri Net Programming Notation", crossref = "PARLE93", pages = "379--390", URL = "http://www.informatik.uni-hildesheim.de/~pep/paper_PEP.html#best_hopkins_bpn2_parle_final", postscript = PS # "best_hopkins_bpn2_parle_final.ps.gz", } @Proceedings{PARLE93, key = "PARLE", booktitle = "{PARLE'93} Parallel Architectures and Languages Europe", title = "{PARLE'93} Parallel Architectures and Languages Europe", editor = "Arndt Bode and Mike Reeve and Gottfried Wolf", month = jun, year = "1993", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "694", } @InProceedings{meseguer-rw90, title = "Rewriting as a Unified Model of Concurrency", author = "Jos\'e Meseguer", year = "1990", month = aug, address = "Amsterdam", booktitle = "Proceedings {C}oncur'90 Conference", series = "Lecture Notes in Computer Science, Volume 458", publisher = "Springer", pages = "384--400", note = "Also, Report SRI-CSL-90-02R, Computer Science Lab, SRI International", } @InProceedings{meseguer96, author = "Jos\'e Meseguer", title = "Rewriting Logic as a Semantic Framework for Concurrency: a Progress Report", booktitle = "Seventh International Conference on Concurrency Theory (CONCUR'96)", month = aug, year = "1996", publisher = "Springer", volume = "1119", series = "Lecture Notes in Computer Science", pages = "331--372", } @TechReport{ncstrl.unipi_it//TR-96-29, bibdate = "September 16, 1996", type = "Technical Report", number = "TR-96-29", institution = "Pisa University, Italy", title = "{DEMOS} at {CONCUR96}", year = "1996", month = aug # " 22,", url = "ftp://ftp.di.unipi.it/pub/techreports/TR-96-29.ps.Z", author = "Corrado - Editor Priami", abstract = "Those that follow are the abstracts of the demonstrations at the CONCUR conference held in Pisa in August 1996. The demonstrations cover different aspects of theory of concurrency. They range from process algebras verifiers to model checkers as well as Petri nets support tools. There are also demonstrations on the check of security properties and performance analysis based on process algebra descriptions. Finally, a demonstration of game aspects with CWB is presented.", postscript = PS # "demos_at_concur96.ps.gz", } @Article{Meseguer:1992:CRL, author = "J. Meseguer", title = "Conditional rewriting logic as a unified model of concurrency", journal = "Theoretical Computer Science", volume = 96, number = 1, pages = "73--155", day = 6, month = apr, year = 1992, coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Sat Nov 22 13:24:22 MST 1997", acknowledgement =ack-nhfb, classification ="C4210 (Formal logic); C6110J (Object-oriented programming); C6110P (Parallel programming)", conflocation = "San Miniato, Italy; 28 Feb.-3 March 1990", conftitle = "2nd Workshop on Concurrency and Compositionality", corpsource = "SRI Int., Menlo Park, CA, USA", keywords = "concurrency control; concurrent programming; concurrent rewriting; cpo; functional programming; high level declarative programming; logical deduction; Maude; object-oriented programming; parallel programming; poset; preorder; programming language; rewriting systems; semantics; standard algebraic models; structural axioms", pubcountry = "Netherlands", treatment = "B Bibliography; P Practical", } @Book{Levine-etal92, key = "Levine, {\em et al}", author = "John Levine and Tony Mason and Doug Brown", title = "Lex and Yacc", publisher = "O'Reilly and Associates, Inc", address = "103 Morris Street, Suite A, Sebastopol, Ca 95472", year = "1992", annote = "10 references.", } @InProceedings{Clavel96, author = "Manuel Clavel and Steven Eker and Patrick Lincoln and Jos\'e Meseguer", title = "Principles of {M}aude", editor = "Jos\'e Meseguer", volume = "4", series = "Electronic Notes in Theoretical Computer Science", pages = "65-89", booktitle = "Proceedings of the First International Workshop on Rewriting Logic", year = "1996", organization = "Elsevier", url = "http://www.csl.sri.com/~clavel/pubs/rwl96b.ps", } @Misc{happy, key = "HAP", title = "Happy, a parser generator for {Haskell}", url = "http://haskell.cs.yale.edu/happy/", } @InCollection{DJ90:htcs, author = "Nachum Dershowitz and Jean-Pierre Jouannaud", year = "1990", title = "Rewrite Systems", booktitle = "Handbook of Theoretical Computer Science", volume = "B: Formal Methods and Semantics", chapter = "6", pages = "243--320", editor = "J. van Leeuwen", publisher = "North-Holland", address = "Amsterdam", } @InProceedings{ClavelMeseguer97, author = "Manuel Clavel and Jos\'e Meseguer", title = "Reflection in rewriting logic and its applications in the Maude language", pages = "128-139", booktitle = "Proceedings of IMSA-97", year = "1997", address = "Japan", note = "Information-Technology Promotion Agency", url = "http://www.csl.sri.com/~clavel/pubs/imsa97.ps", } @INPROCEEDINGS{grahlmann:6a/97, AUTHOR = {Bernd Grahlmann}, booktitle = "Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97)", MONTH = jun, PAGES = {440--443}, PUBLISHER = {Springer}, SERIES = {Lecture Notes in Computer Science}, TITLE = {The PEP Tool}, VOLUME = {1254}, YEAR = {1997}, url = "http://www.informatik.uni-hildesheim.de/~pep/paper_PEP.html#grahlmann_pep_cav97", } @Misc{ConMailingList, key = "CML", title = "The Concurrency Mailing List", url = "http://www.cwi.nl/~bertl/concurrency/concurrency.html", } @TechReport{LeuckerTobies98, author = "Martin Leucker and Stephan Tobies", title = "Truth---A Platform for Verification of Distributed Systems", institution = "RWTH Aachen", abstract = "Formal Methods are becoming more an more important for the development of hardware and software systems. Verification tools support the employment of Formal Methods. This paper gives an overview of the design and implementation of the verification tool Truth. We define and explain requirements for verification tools. Furthermore, we discuss several semantic models, specification languages and logics and their visualisation from a tool builder's perspective and show how these requirements were adopted in Truth.", keywords = "formal methods, verification, specification, temporal logic, tool", year = "1998", number = "98-05", month = May, URL = "http://aib.informatik.rwth-aachen.de/1998/index.html", postscript = Documents # "Leucker/truth.ps.gz" } @Unpublished{Leucker98, author = "Martin Leucker", title = "Rewriting Logic as a Framework for Building Generic Tools for Verifying Concurrent Systems", institution = "RWTH Aachen", year = "1998", note = "Unpublished", postscript = Documents # "Leucker/generic_tools.ps.gz", } @Article{BurEsp97, author = "Burkart and Esparza", title = "More Infinite Results", journal = "BEATCS: Bulletin of the European Association for Theoretical Computer Science", volume = "62", year = "1997", location = "printed copy", url = "http://www.elsevier.nl/locate/entcs/volume6.html", } @Misc{Stirling97, author = "C. Stirling", title = "Games for bisimulation and model checking", year = "1997", month = jun, note = "Notes for Mathfit instructional meeting on games and computation, Edinburgh", postscript = PS # "stirling__games.ps.gz", url = "http://www.dcs.ed.ac.uk/home/cps/mathfit.ps", } @Book{Burkart97:LNCS, author = "Olaf Burkart", title = "Automatic Verification of Sequential Infinite-State Processes", volume = "1354", publisher = "Springer", address = "New York, NY, USA", year = "1997", ISBN = "3-540-63982-9", series = "Lecture Notes in Computer Science", } @TechReport{FrohlichMa1994a, author = "M. Fr{\"o}hlich and M. Werner", institution = "Department of Computer Science; University of Bremen", title = "The Graph Visualization System da{V}inci - {A} User Interface for Applications", year = "1994", url = "ftp://ftp.Uni-Bremen.DE/pub/graphics/daVinci/papers/techrep0594.ps.gz", keywords = "implemented in ASpecT", month = sep, number = "5/94", scope = "appl", } @Article{Wirsing:1995:ASL, author = "M. Wirsing", title = "Algebraic Specification Languages: An Overview", journal = "Lecture Notes in Computer Science", volume = "906", pages = "81--??", year = "1995", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, } @Book{Thompson96, author = "Simon Thompson", title = "The Craft of Functional Programming", publisher = "Addison-Wesley", year = "1996", ISBN = "0-201-40357-9", abstract = "A textbook for beginners, learning Haskell as first programming language.", } @Book{Hoare:csp, title = "Communcating Sequential Processes", publisher = "Prentice Hall", year = "1985", author = "C. A. R. Hoare", } @TechReport{PlotkinSOS81, author = "Gordon D Plotkin", title = "A {S}tructural {A}pproach to {O}perational {S}emantics", number = "FN-19", institution = "DAIMI, University of Aarhus, Denmark", month = sep, year = "1981", } @InProceedings{CONCUR::BurkartCS1996, title = "Bisimulation Collapse and the Process Taxonomy", author = "Olaf Burkart and Didier Caucal and Bernhard Steffen", pages = "247--262", booktitle = "CONCUR'96: Concurrency Theory, 7th International Conference", editor = "Ugo Montanari and Vladimiro Sassone", address = "Pisa, Italy", month = "26--29~" # aug, year = "1996", series = "Lecture Notes in Computer Science", volume = "1119", publisher = "Springer", ISBN = "ISBN 3-540-61604-7", location = "printed copy", postscript = PS # "burkart_bisim_collapse.ps.gz", } @InCollection{Fit:basml, author = "Melvin C. Fitting", title = "Basic Modal Logic", editor = "Dov M. Gabbay and C. J. Hogger and J. A. Robinson", booktitle = "Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 1: Logical Foundations", pages = "368--448", publisher = "Clarendon Press", address = "Oxford", year = "1993", } @Book{DiekertRozenberg95, editor = "Volker Diekert and Grzegorz Rozenberg", publisher = "World Scientific", address = "Singapore", title = "The Book of Traces", year = "1995", } @InProceedings{CONCUR::Bradfield1996, title = "The Modal mu-calculus Alternation Hierarchy Is Strict", author = "J. C. Bradfield", pages = "233--246", booktitle = "CONCUR'96: Concurrency Theory, 7th International Conference", editor = "Ugo Montanari and Vladimiro Sassone", address = "Pisa, Italy", month = "26--29~" # aug, year = "1996", series = "Lecture Notes in Computer Science", volume = "1119", publisher = "Springer", ISBN = "ISBN 3-540-61604-7", } @InProceedings{Viry:1994:REM, author = "Patrick Viry", title = "Rewriting: An Effective Model of Concurrency", booktitle = "Proceedings of {PARLE}'94 -- Parallel Architectures and Languages Europe", series = "Lecture Notes in Computer Science", volume = "817", pages = "648--660", year = "1994", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon May 13 11:52:14 MDT 1996", acknowledgement = ack-nhfb, publisher = "Springer", } @TechReport{Viry96, author = "Patrick Viry", title = "A Rewriting Implementation of pi-calculus", institution = "Dipartimento di Informatica", number = "TR-96-30", month = mar # " 26", year = "1996", keywords = "pi-calculus, rewriting", url = "ftp://ftp.di.unipi.it/pub/techreports/TR-96-30.ps.Z", abstract = "We introduce a rewriting implementation of the reduction relation of \$$\backslash$pi\$-calculus and prove its correctness. The implementation is based on terms with De Bruijn indices and an explicit substitution operator. The resulting rewrite rules need to be applied modulo a large and complex equational theory, and are only of theoretical interest. Applying the coherence techniques introduced in a previous paper, we transform this specification into an equivalent one that only requires rewriting modulo associativity and commutativity. This latter rewrite system can then be straightforwardly encoded in currently available rewriting-based programming languages. Finally, we sketch a possible application of this implementation as the basis for adding input-output capabilities to such languages.", } @TechReport{Viry95, author = "Patrick Viry", title = "Rewriting modulo a rewrite system", institution = "Dipartimento di Informatica, Universita di Pisa", number = "TR-95-20", month = dec # " 01", year = "1995", url = "ftp://ftp.di.unipi.it/pub/techreports/TR-95-20.ps.Z", abstract = "We introduce rewriting with two sets of rules, the first interpreted equationally and the second not. A semantic view considers equational rules as defining an equational theory and reduction rules as defining a rewrite relation modulo this theory. An operational view considers both sets of rules as similar. We introduce sufficient properties for these two views to be equivalent (up to different notions of equivalence). The paper ends with a collection of example showing the effectiveness of this approach.", } @InProceedings{BKKMV96, author = "P.~Borovansky and C.~Kirchner and H.~Kirchner and P.E.~Moreau and M.~Vittek", title = "ELAN: A Logical Framework Based on Computational Systems", booktitle = "Proc.\ of the First Int.\ Workshop on Rewriting Logic", series = "Electronic Notes in Theoretical Computer Science", volume = "4", year = "1996", publisher = "Elsevier", url = "http://www1.elsevier.nl/mcs/tcs/pc/volume4.htm" } @TechReport{Peterson96, author = "John Peterson and Kevin Hammond and others", title = "Report on the programming language {Haskell}, a non-strict purely-functional programming language, Version 1.3", institution = "Yale University", year = "1996", month = may, url = "ftp://haskell.org/pub/report/report13.ps.gz", } @InProceedings{Launchbury94, author = "J. Launchbury and S. Peyton Jones", title = "Lazy Functional State Threads", year = "1994", abstract-url = "http://www.cse.ogi.edu/~jl/biblio.html", address = "Orlando", url = "http://www.cse.ogi.edu/~jl/Papers/stateThreads.ps", publisher = "ACM Press", scope = "impmonads", booktitle = "Programming Languages Design and Implementation", location = "printed copy" } @MastersThesis{Tobies98, author = "Stephan Tobies", title = "Design und {I}mplementierung einer {P}lattform zur {V}erifikation verteilter {S}ysteme", school = "Aachen, University of Technology", year = "1998", note = "(German)", postscript = PS # "tobies__diplom.ps.gz", } @InProceedings{LICS::DziembowskiJW1997, title = "How Much Memory Is Needed to Win Infinite Games?", author = "Stefan Dziembowski and Marcin Jurdzi{\'n}ski and Igor Walukiewicz", pages = "99--110", booktitle = "Proceedings, Twelth Annual {IEEE} Symposium on Logic in Computer Science", year = "1997", month = "29~" # jun # "--2~" # jul, address = "Warsaw, Poland", organization = "IEEE Computer Society Press", references = "\cite{ICALP::AbadiLW1989} \cite{ICALP::BradfieldEM1996} \cite{CAAP::Dam1992} \cite{FOCS::emersonJ1988} \cite{FOCS::EmersonJ1991} \cite{STOC::GurevichH1982} \cite{LICS::Klarlund1992} \cite{STACS::MalerPS1995} \cite{APAL::McNaughton1993} \cite{APAL::NerodeRY1996} \cite{POPL::PnueliR1989} \cite{STACS::thomas1995} \cite{LICS::Walukiewicz1995}", location = "printed copy", postscript = PS # "walukiewicz__how_much_memory.ps.gz", } @InProceedings{Walukiewicz98, author = "Igor Walukiewicz", title = "Difficult configurations - on the complexity of {LTrL}", editor = "K.G. Larsen and S. Skyum and G. Winskel", volume = "1443", series = "Lecture Notes in Computer Science", pages = "140--151", booktitle = "Proceedings of 25th International Colloquium on Automata, Languages and Programming (ICALP'98)", year = "1998", postscript = PS # "walukiewicz__difficult_configurations.ps.gz", url = "http://www.brics.dk/~igw/icalp98.ps", } @Article{Walukiewicz99, author = {Igor Walukiewicz}, title = {Difficult Configurations -- On the Complexity of {LTrL}}, journal = {Formal Methods in System Design}, year = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, note = {to appear}, annote = {extended version of ICALP'98 paper}, postscript = PS # "walukiewicz__difficult_conf_full99.ps.gz", } @MastersThesis{Leucker96, author = "Martin Leucker", title = "Comparison of two semantic approaches to unification", school = "RWTH Aachen", year = "1996", abstract = "The master theses compares the two most prominent semantic approaches to unifica tion. We can show that unification in primal algebras is not a direct instance of unification in monoidal theories. However, it is possible to reduce unification in a given primal algebra to unification in a corresponding monoidal theory. As by-products of this work we have shown that unification in algebras is an instance of unification modulo equational theories, and we have introduced a new notion of equivalence for equational theories.", location = "printed copy", postscript = Documents # "Leucker/diplom.ps.gz", } @TechReport{MeseguerJ:rewllsf, author = "Narciso Mart{\`\i}-Oliet and Jos\'e Meseguer", title = "Rewriting Logic as a Logical and Semantical Framework", institution = "SRI International", year = "1993", number = "SRI-CSL-93-05", month = aug, keywords = "rewriting", } @InProceedings{MeseguerFW92, author = "Jos\'e Meseguer and Kokichi Futatsugi and Timothy Winkler", title = "Using rewriting logic to specify, program, integrate, and reuse open concurrent systems of cooperating agents.", pages = "61--106", booktitle = "Proceedings of the 1992 International Symposium on New Models for Software Architecture", year = "1992", organization = "Research Institute of Software Engineering", address = "Tokyo, Japan", } @InProceedings{LescanneALP90, author = "P. Lescanne", title = "Implementation of Completion by Transition Rules + Control: {{\sc ORME}}", pages = "262--269", booktitle = "Algebraic and Logic Programming, Second International Conference, Nancy, France, October 1990, Proceedings", year = "1990", editor = "H. Kirchner and W. Wechler", volume = "463", publisher = "Springer", address = "Berlin-Heidelberg-New York", series = "Lecture Notes in Computer Science", } @InCollection{Klop92, author = "Jan Willem Klop", year = "1992", title = "Term Rewriting Systems", booktitle = "Handbook of Logic in Computer Science", editor = "S. Abramsky and D. M. Gabbay and T. S. E. Maibaum", publisher = "Oxford University Press", volume = "2", chapter = "1", pages = "1--117", address = "Oxford", } @Article{Wadler:1997:HDI, author = "Philip Wadler", title = "How to declare an imperative", journal = "ACM Computing Surveys", volume = "29", number = "3", pages = "240--263", month = sep, year = "1997", coden = "CMSVAN", ISSN = "0360-0300", bibdate = "Wed Oct 22 18:05:34 MDT 1997", url = "http://www.acm.org:80/pubs/citations/journals/surveys/1997-29-3/p240-wadler/", abstract = "How can we integrate interaction into a purely declarative language? This tutorial describes a solution to this problem based on a monad. The solution has been implemented in the functional language Haskell and the declarative language Escher. Comparisons are given with other approaches to interaction based on synchronous streams, continuations, linear logic, and side effects.", acknowledgement = ack-nhfb, keywords = "theory", subject = "{\bf D.3.3} Software, PROGRAMMING LANGUAGES, Language Constructs and Features, Input/Output. {\bf F.4.1} Theory of Computation, MATHEMATICAL LOGIC AND FORMAL LANGUAGES, Mathematical Logic, Lambda calculus and related systems.", } @InProceedings{PHH*93, author = "Simon L. Peyton Jones and Cordy Hall and Kevin Hammond and Will Partain and Phil Wadler", title = "{The Glasgow Haskell Compiler: A Technical Overview}", booktitle = "Joint Framework for Information Technology Technical Conference", address = "Keele", year = "1993", owner = "pcl", descr = "plfun", postscript = PS # "haskell/grasp-jfit.ps.Z" } @InProceedings{MFCS::Niebert1995, title = "A {$\nu$}-Calculus with Local Views for Systems of Sequential Agents", author = "Peter Niebert", editor = "Jir{\'\i} Wiedermann and Petr H{\'a}jek", booktitle = "Mathematical Foundations of Computer Science 1995, 20th International Symposium", address = "Prague, Czech Republic", month = "1~" # sep # "-- 28~" # aug, year = "1995", series = "lncs", volume = "969", publisher = "Springer", pages = "563--573", } @Proceedings{Steffen:1998:TAC, editor = "Bernhard Steffen", booktitle = "Tools and algorithms for the construction and analysis of systems: 4th International Conference, {TACAS}'98, held as part of the joint European Conferences on Theory and Practice of Software, {ETAPS}'98, Lisbon, Portugal, March\slash April 1998, proceedings", title = "Tools and algorithms for the construction and analysis of systems: 4th International Conference, {TACAS}'98, held as part of the joint European Conferences on Theory and Practice of Software, {ETAPS}'98, Lisbon, Portugal, March\slash April 1998, proceedings", volume = "1384", publisher = "Springer", address = "New York, NY, USA", pages = "various", year = "1998", coden = "LNCSD9", ISBN = "3-540-64356-7 (paperback)", ISSN = "0302-9743", LCCN = "QA76.9.S88T33 1998", bibdate = "Mon Apr 27 17:37:18 MDT 1998", series = "Lecture Notes in Computer Science", acknowledgement = ack-nhfb, keywords = "Computer software -- Development -- Congresses; System design -- Congresses", } @InProceedings{StevensStirling98, author = "Perdita Stevens and Colin Stirling", booktitle = "Proceedings of the 4th International Conference on Tools and algorithms for the construction and analysis of systems (TACAS'98)", title = "Practical Model-Checking using Games", editor = "B. Steffen", volume = "1384", publisher = "Springer", address = "New York, NY, USA", pages = "85--101", year = "1998", coden = "LNCSD9", ISBN = "3-540-64356-7 (paperback)", ISSN = "0302-9743", LCCN = "QA76.9.S88T33 1998", bibdate = "Mon Apr 27 17:37:18 MDT 1998", series = "Lecture Notes in Computer Science", } @Article{JFP::Hill1996, title = "Combinators for parsing expressions", author = "Steve Hill", pages = "445--463", journal = "Journal of Functional Programming", month = may, year = "1996", volume = "6", number = "3", } @Article{HuttonGraha98, author = "Graham Hutton and Erik Meijer", journal = "Journal of Functional Programming", title = "Monadic Parsing in {Haskell}", year = 1998, volume = 8, number = 4, url = "http://www.cs.nott.ac.uk/Department/Staff/gmh/bib.html#pearl", keywords = "monads, parsing, Haskell", scope = "pearls", } @INPROCEEDINGS{LLNT98, AUTHOR = {M.~Lange and M.~Leucker and T.~Noll and S.~Tobies}, TITLE = {Truth -- A Verification Platform for Concurrent Systems}, BOOKTITLE = {Proceedings of Tools'98}, YEAR = {1998}, PUBLISHER = {Christian-Albrechts University of Kiel}, abstract = "We briefly explain the design and implementation of the newly developed tool \Truth which serves as a general platform for the systematic investigation of different specification languages, semantic models, and logics for concurrent systems, supported by enhanced visualization capabilities. Modularity is achieved by employing the rewriting logic approach as a semantic framework for concurrency. Further extensions of \Truth, being in the design stage, comprise the support of the trace model of concurrency as well as game--base model checking algorithms.", url = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/tools98.ps.gz", postscript = PS # "tools98.ps.gz", } @InCollection{LLNT98b, AUTHOR = {M.~Lange and M.~Leucker and T.~Noll and S.~Tobies}, TITLE = {Truth -- A Verification Platform for Concurrent Systems}, BOOKTITLE = {Tool Support for System Specification, Development, and Verification}, YEAR = 1999, PUBLISHER = "Springer", address = "Wien New York", series = "Advances in Computing Science", abstract = "We briefly explain the design and implementation of the newly developed tool \Truth which serves as a general platform for the systematic investigation of different specification languages, semantic models, and logics for concurrent systems, supported by enhanced visualization capabilities. Modularity is achieved by employing the rewriting logic approach as a semantic framework for concurrency. Further extensions of \Truth, being in the design stage, comprise the support of the trace model of concurrency as well as game--base model checking algorithms.", } @Book{Armstrong93, author = "J. Armstrong and M. Williams and R. Virding", title = "Concurrent Programming in Erlang", publisher = "Prentice-Hall", address = "Englewood Cliffs, NJ", year = "1993", keywords = "functional parallel input output i/o", ISBN = "0-13-285792-8", abstract = "Erlang is a concurrent functional programming language designed for large industrial real-time systems. Erlang is dynamically typed and has a pattern matching syntax. Functions are defined using recursion equations. Erlang provides explicit concurrency, has asynchronous message passing and is relatively free from side effects. Distributed Erlang programs can run transparently on cross-platform multi-vendor systems. The language has primitives for detecting run-time errors and for dynamic code replacement (i.e. changes to code can be made in a running real-time system, without stopping system).", } @INPROCEEDINGS{LN99, AUTHOR = "M. Leucker and T. Noll", TITLE = {Rapid Prototyping of Specification Language Implementations}, BOOKTITLE = {Proceedings of the 10th IEEE International Workshop on Rapid System Prototyping}, YEAR = 1999, PUBLISHER = {IEEE Computer Society Press}, pages = "60--65", abstract = "Specification languages such as LOTOS and SDL play an important r\^ole in the design and implementation of distributed systems. Their for\-mal syntax and semantics supports the development of compilers and of verification tools. This paper introduces a generic and uniform approach to support such languages in verification tools. We present a compiler generator which, given the description of a specification language, automatically generates a corresponding implementation. More specifically, the syntax and semantics of the specification language has to be defined using Meseguer's Rewriting Logic formalism, a unified semantic framework for concurrency. From this description a compiler is derived which parses a given system specification and computes the corresponding semantic object, such as a labelled transition system. The latter can be processed further in subsequent analysis and verification phases. Thus we propose some kind of ``meta--pro\-to\-typing'' approach in the sense that new specification formalisms for distributed systems can easily be tested without the need to develop an implementation by hand.", } @TECHREPORT{MPI93, AUTHOR = {The Message Passing Interface Forum}, TITLE = {Document for a {S}tandard {M}essage-{P}assing {I}nterface}, INSTITUTION = {University of Tennessee}, TYPE = {{CS}-93-214}, MONTH = 11, YEAR = 1993 } @Manual{cvs-man, author = "Per Cederqvist", title = "Version Management with {CVS}", organization = "Signum Support AB", year = "1993", month = nov, address = "Box 2044, S-580 02 Linkoping, Sweden", url = "http://www.loria.fr/~molli/cvs/cvs-0.9/cvs_toc.html#SEC3", keywords = ":cvs:scm:", } @InProceedings{VardiWolper86, author = "M. Y. Vardi and P. Wolper", title = "An Automata-Theoretic Approach to Automatic Program Verification", pages = "332--345", booktitle = "Symposium on Logic in Computer Science ({LICS}'86)", month = jun, publisher = "IEEE Computer Society Press", address = "Washington, D.C., USA", year = "1986", ISBN = "0-8186-0720-3", } @InProceedings{DanGiuVardi99, author = "M. Daniele and F. Giunchiglia and M. Y. Vardi", title = "Improved Automata Generation for Linear Temporal Logic", booktitle = "Proc. of 11th Inter. Conf. on Computer-Aided Verification (CAV'99)", year = "1999", } @Article{Dam:1994:CEF, author = "M. Dam", title = "{CTL}* and {ECTL}* as fragments of the modal $\mu$-calculus", journal = "Theoretical Computer Science", volume = "126", number = "1", pages = "77--96", day = "11", month = apr, year = "1994", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Sat Nov 22 13:15:15 MST 1997", acknowledgement = ack-nhfb, classification = "C4210 (Formal logic); C4220 (Automata theory); C4240 (Programming and algorithm theory)", corpsource = "Swedish Inst. of Comput. Sci., Kista, Sweden", keywords = "admissibility criterion; automata theory; Buchi automata; computational complexity; CTL*; ECTL*; formula representation; full branching-time CTL*; infinite strings; linear time; linear-time fragment; modal base logic; modal mu -calculus; temporal logic", pubcountry = "Netherlands", treatment = "T Theoretical or Mathematical", } @InCollection{tho90handbook, author = "Wolfgang Thomas", booktitle = "Handbook of Theoretical Computer Science", chapter = "4", editor = "J. van Leeuwen", pages = "133--191", publisher = "Elsevier Science Publishers B. V.", title = "Automata on Infinite Objects", year = "1990", volume = {B}, annote = "This chapter gives a comprehensive overview on automata theory and logic on infinite words and infinite trees.", } @InProceedings{BreiLooPrie98, author = "Silvia Breitinger and Rita Loogen and Steffen Priebe", title = "Parallel Programming with {Haskell} and {MPI}", editor = "Hammond and Davie", pages = "135--154", booktitle = "Proceedings of the 10th International Workshop on Implementation of Functional Languages", year = "1998", organization = "University of London, UK", month = "September", } @Unpublished{Stirling96-2, author = "Colin Stirling", title = "Decidability of Bisimulation Equivalence for Normed Pushdown Processes", note = "extended version of LNCS 1119", location = "printed copy", url = "http://www.dcs.ed.ac.uk/~cps/pda.ps", } @Article{Stevens:1998:AGI, author = "P. Stevens", title = "Abstract Games for Infinite State Processes", journal = "Lecture Notes in Computer Science", volume = "1466", pages = "147--??", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat Oct 10 14:40:24 MDT 1998", acknowledgement = ack-nhfb, location = "printed copy", url = "http://www.dcs.ed.ac.uk/~pxs/vmcai98.ps", } @Unpublished{Stirling96-3, author = "Colin Stirling", title = "Model Checking and Other Games", note = "Notes for Mathfit Workshop on Finite Model Theory", year = "1996", location = "printed copy", url = "http://www.dcs.ed.ac.uk/~cps/mfit.ps", } @Unpublished{FechtSeidl97, author = "Christian Fecht and Helmut Seidel", title = "A Faster Solver for General Systems of Equations", note = "Preprint submitted to Elsevier", OPTyear = "1997", location = "printed copy", } @InProceedings{DiekertGastin99, author = "Volker Diekert and Paul Gastin", title = "An expressively complete temporal logic without past tense operators for {M}azurkiewicz traces", abstract = "Mazurkiewicz traces are a widely accepted model of concurrent systems. We introduce a linear time temporal logic which has the same expressive power as the first order theory of finite (infinite resp.) traces. The main contribution of the paper is that we only use future tense modalities in order to obtain expressive completeness. Our proof is direct and uses no reduction to words. As a formal consequence Kamp's theorem for both finite and infinite words becomes a corollary. This direct approach became possible due to a new proof technique of Wilke developed for the case of finite words.", OPTeditor = "", OPTvolume = "", OPTnumber = "", series = "Lecture Notes in Computer Science", OPTpages = "", booktitle = "Proceedings of CSL'99", year = "1999", OPTorganization = "", OPTpublisher = "", OPTaddress = "", OPTmonth = "", OPTnote = "", OPTannote = "", postscript = PS # "diekert_gastin__expressive_complete.ps.gz", } @TechReport{GastinMeyerPetit98, author = "P. Gastin and R. Meyer and A. Petit", title = "A (non-elementary) modular decision procedure for {LTrL}", institution = "LSV, ENS de Cachan", year = "1998", note = "extended version of MFCS'98", url = "http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/rr-lsv-1998-5.rr.ps", postscript = PS # "gastin_meyer_petit__decision_LTrL.ps.gz", } @InProceedings{GasMeyPet98, author = "P. Gastin and R. Meyer and A. Petit", title = "A (Non-elementary) Modular Decision Procedure for {LTrL}", booktitle = "MFCS: Symposium on Mathematical Foundations of Computer Science", year = "1998", series = "Lecture Notes in Computer Science", volume = "1450", } @INPROCEEDINGS{L99, author = "M. Leucker", title = {Model Checking Games for the Alternation Free mu-Calculus and Alternating Automata}, booktitle = {Proceedings of the 6th International Conference on Logic for Programming and Automated Reasoning "(LPAR'99)"}, YEAR = 1999, PUBLISHER = "Springer", editor = "Harald Ganzinger and David McAllester and Andrei Voronkov", pages = "77--91", volume = "1705", series = "Lecture Notes in Artificial Intelligence", abstract = "We relate game-based model checking and model checking via {\em 1-letter simple weak alternating {B}{\"u}chi automata} (1SWABA) for the {\em altern\-ation-free $\mu$-calculus}. Game-based algorithms have the advantage that in addition to checking whether a formula is valid or not they determine a winning strategy which can be employed for explaining to the user why the formula is valid or not. 1SWABA are a restricted class of alternating {B}{\"u}chi automata and were defined in \cite{BVW94}. They admit efficient automata-based model checking for CTL and the alternation-free $\mu$-calculus. We give an interpretation for these automata in terms of game theory and show that this interpretation coincides with the notion of model checking games for CTL and the $\mu$-calculus. Then we explain that the efficient non-emptiness procedure for 1SWABA presented in \cite{BVW94} can also be understood as a game-based model checking procedure. Furthermore, we show that this algorithm is not only useful for checking the validity of a formula but also for determining a {\em winning strategy} for the winner of the underlying model checking game. In this way we obtain a linear time algorithm for model checking games.", url = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker__Games_Automata_mu_calculus.ps.gz", postscript = Documents # "Leucker/games_automata_mu_calculus.ps.gz", } @Article{MukundThiagarajan96, author = "M. Mukund and P. S. Thiagarajan", title = "Linear time temporal logics over {Mazurkiewicz} traces", journal = "Lecture Notes in Computer Science", volume = "1113", pages = "62--92", year = "1996", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon Aug 25 16:49:05 MDT 1997", acknowledgement = ack-nhfb, annote = "Also known as MFCS'96", keywords = "computer science; informatics; mathematical foundations; MFCS", } @InProceedings{HenriksenThiagarajan97, title = "A Product Version of Dynamic Linear Time Temporal Logic", author = "Jesper G. Henriksen and P. S. Thiagarajan", pages = "45--58", booktitle = "CONCUR'97: Concurrency Theory, 8th International Conference", editor = "Antoni Mazurkiewicz and J{\'o}zef Winkowski", address = "Warsaw, Poland", month = "1--4~" # jul, year = "1997", series = "Lecture Notes in Computer Science", volume = "1243", publisher = "Springer", ISBN = "ISBN 3-540-63141-0", } @InProceedings{Thiagarajan95, title = "A Trace Consistent Subset of~{PTL}", author = "P. S. Thiagarajan", pages = "438--452", booktitle = {Proceedings of the 6th International Conference on Concurrency Theory (CONCUR'95)}, editor = "Insup Lee and Scott A. Smolka", address = "Philadelphia, Pennsylvania", month = "21--24~" # aug, year = "1995", series = "Lecture Notes in Computer Science", volume = "962", publisher = "Springer", ISBN = "ISBN 3-540-60218-6", } @Book{DiaFut98, author = "R. Diaconescu and K. Futatsugi", title = "Cafe{OBJ} Report", publisher = "World Scientific", address = "Singapore", year = "1998", ISBN = "981-02-3513-5", descriptor = "Beweiser, Modell, Specification language", annote = "CafeOBJ is an industrial strength modern algebraic specification language, a successor of the famous OBJ language, and directly incorporationg new paradigms such as behavioral concurrent specification and rewriting logic. CafeOBJ is the core of an environment supporting the systems (mainliy software but not only) development process at several levels, including prototyping, specification, and formal verification.", } @INPROCEEDINGS{Noll99, AUTHOR = {T.~Noll}, TITLE = {On Coherence Properties in Term Rewriting Models of Concurrency}, BOOKTITLE = {Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99)}, YEAR = {1999}, PUBLISHER = {Springer}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {1664}, PAGES = {478--493}, } @Article{HS87, author = "A. Herold and J. J. Siekmann", key = "Herold\&{}Siekmann", journal = "Journal of Automated Reasoning", title = "Unification in {A}belian Semigroups", year = "1987", month = sep, volume = "3", number = "3", pages = "247--284", location = "E\&{}S Library", } @Article{Huet78, author = "G. Huet", year = "1978", journal = "Information Processing Letters", number = "3", pages = "144--147", title = "An Algorithm to Generate the Basis of Solutions to Homogenous Linear Diophantine Equations", volume = "7", } @InCollection{For86, author = "A. Fortenbacher", editor = "J. P. Jouannaud", title = "An Algebraic Approach to Unification Under Associativity and Commutativity", booktitle = "Rewriting Techniques and Applications", series = "Lecture Notes in Computer Science", volume = "202", pages = "381--397", publisher = "Springer", address = "Berlin-Heidelberg-New York", year = "1986", keywords = "AI14 AI11", } @Article{Sti81, author = "Mark E. Stickel", title = "A Unification Algorithm for Associative-Commutative Functions", journal = "Journal of the ACM", volume = "28", number = "2", pages = "423--434", month = apr, year = "1981", coden = "JACOAH", ISSN = "0004-5411", bibdate = "Tue Oct 25 22:33:21 1994", acknowledgement = ack-nhfb, keywords = "Logic", } @Article{MiddeldorpHamoen94, author = "A.~Middeldorp and E.~Hamoen", title = "Completeness Results for Basic Narrowing", journal = "Journal of Applicable Algebra in Engineering, Communication and Computing", volume = "5", pages = "313--353", year = "1994", } @Book{BaaderNipkow98, author = "Franz Baader and Tobias Nipkow", title = "Term Rewriting and All That", publisher = "Cambridge University Press", address = "New York", year = "1998", ISBN = "0-521-45520-0", descriptor = "Unifikation, Groebner Basis, Konfluenz, Universelle Algebra, Reduktionssystem", annote = "Elemente der Logik, der universellen Algebra, von automatischen Beweissystemen, sowie funktionaler Programmierung fliessen hier zusammen. Sonst nur in Konferenzberichten und spezialisierten Zeitschriften veroeffentlichtes Material wird hier erstmals in Lehrbuchform zugaenglich gemacht.", } @MastersThesis{vanHuellen99, author = "Philipp van H{\"u}llen", title = "Design und {I}mplementierung eines {S}pezifikationssprachencompilers", school = "Aachen, University of Technology", year = "1999", note = "(German)", postscript = PS # "vanHuellen__diplom.ps.gz", } @MastersThesis{Lange99, author = "Martin Lange", title = "Spielbasiertes {M}odel-{C}hecking f{\"u}r den alternierungsfreien mu-{K}alk{\"u}l", school = "Aachen, University of Technology", year = "1999", note = "(German)", postscript = PS # "lange__diplom.ps.gz", } @InProceedings{Alur:1998:DGP, author = "R. Alur and K. McMillan and D. Peled", title = "Deciding Global Partial-Order Properties", editor = "K.G. Larsen and S. Skyum and G. Winskel", booktitle = "Proceedings of 25th International Colloquium on Automata, Languages and Programming (ICALP'98)", series = "Lecture Notes in Computer Science", volume = "1443", pages = "41--52", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat Oct 10 14:40:24 MDT 1998", url = "http://link.springer.de/link/service/series/0558/tocs/t1443.htm" } @Article{MPW92, author = "Robin Milner and Joachim Parrow and David Walker", title = "A Calculus of Mobile Processes, {P}arts {I} and {II}", journal = "Information and Computation", year = 1992, volume = 100, pages = "1--77", month = sep, } @Book{Quinn94, author = "Michael J. Quinn", title = "Parallel computing: Theory and Practice", publisher = "McGraw-Hill", year = 1994, address = "New York", edition = 2, } @InProceedings{Muscholl99, author = "A. Muscholl", title = "Matching Specifications for Message Sequence Charts", pages = "273--287", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Tue Sep 14 06:09:05 MDT 1999", acknowledgement = ack-nhfb, keywords = "computation structures; ETAPS; FOSSACS; software science", publisher = "Springer", booktitle = "Foundations of Software Science and Computation Structures (FoSSaCS'98)", year = "1998", } @InProceedings{MSP98, author = "Anca Muscholl and Zhendong Su and Doron Peled", title = "Deciding Properties for Message Sequence Charts", booktitle = "Foundations of Software Science and Computation Structures (FoSSaCS'98)", address = "Lisbon, Portugal", publisher = "Springer", year = "1998", series = "Lecture Notes in Computer Science", volume = "1578", } @InProceedings{MP99, author = "Anca Muscholl and Doron Peled", editor = "Tomasz Wierzbicki {Miroslaw Kutylowski, Leszek Pacholski}", title = "Message Sequence Graphs and Decision Problems on {M}azurkiewicz Traces", booktitle = "Mathematical Foundations of Computer Science 1999, 24th International Symposium, MFCS'99, Szklarska Poreba, Poland, September 6-10, 1999, Proceedings.", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1672", year = "1999", ISBN = "3-540-66408-4", } @Article{Levi99, author = "Levi", title = "A Compositional mu-calculus Proof System for Statecharts Processes", journal = "TCS: Theoretical Computer Science", volume = "216", year = "1999", } @InProceedings{EJS92, author = "E. A. Emerson and C. S. Jutla and A. P. Sistla", title = {On model-checking for fragments of the $\mu$-calculus}, booktitle = "Unknown", year = "1992", location = "printed copy", } @TechReport{Hayes93, author = "I. J. Hayes and C. B. Jones and J. E. Nicholls", title = "Understanding the differences between {VDM} and {Z}", institution = "University of Manchester, Computer Science Department", number = "UMCS-93-8-1", month = aug, year = "1993", url = "ftp://ftp.cs.man.ac.uk/pub/TR/UMCS-93-8-1.ps.Z http://www.cs.man.ac.uk/csonly/cstechrep/Abstracts/UMCS-93-8-1.html mailto:techreports@cs.man.ac.uk", abstract = "This paper attempts to provide an understanding of the interesting differences between two well-known specification languages. The main ideas are presented in the form of a discussion. This was partly prompted by Lakatos' book `Proof and Refutations' but since this paper is less profound, characters from the childrens' television series `The Magic Roundabout' are the speakers: Zebedee speaks for Z, Dougal puts the VDM position, and Florence acts as the user. The specifications which are presented have been made similar so as to afford comparison - in neither the VDM nor the Z case would they be considered to be ideal presentations. Some technical details are relegated to footnotes.", } @TechReport{ercim.sics//R94-09, title = "A polynomial-time algorithm for deciding bisimilation equivalence of normed Basic Parallel Processes", type = "Technical Report", number = "R94-09", keywords = "Process algebra; Formal languages; Analysis of algorithms.", pages = "11", bibdate = "April 6, 1994", year = 1994, url = "ftp://ftp.sics.se/pub/SICS-reports/Reports/SICS-R--94-09--SE.ps.Z", author = "Yoram Hirshfeld and Mark Jerrum and Faron Moller", abstract = "A polynomial-time algorithm is presented for deciding bisimulation equivalence of so-called Basic Parallel Processes: multisets of elementary processes combined by a commitative parallel-composition operator.", institution = "Swedish Institute of Computer Science", } @Article{ThiagarajanHen98, author = "P. S. Thiagarajan and J. G. Henriksen", title = "Distributed Versions of Linear Time Temporal Logic: {A} Trace Perspective", journal = "Lecture Notes in Computer Science", volume = "1492", pages = "643--681", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Tue Sep 14 12:24:05 MDT 1999", acknowledgement = ack-nhfb, keywords = "petri nets", } @InProceedings{HenLeu99, author = "J. Henriksen and M. Leucker", title = "The Automata-Theoretic Approach Works for Global Trace Logics", booktitle = "Proceedings of the 11th Nordic Workshop on Programming Theory", year = 1999, month = Oct, organization = "Uppsala University", } @INPROCEEDINGS{Nol99, AUTHOR = {T.~Noll}, TITLE = {Koh\"arenzeigenschaften in termersetzungsbasierten Modellen f\"ur verteilte Systeme}, BOOKTITLE = {9.~Theorietag der GI--Fachgruppe 0.1.5 ``Automaten und Formale Sprachen''}, EDITOR = {F.~Otto and G.~Niemann}, YEAR = {1999}, PUBLISHER = {University of Kassel}, SERIES = {Preprint}, VOLUME = {12/99}, PAGES = {52}, } @INPROCEEDINGS{L99b, AUTHOR = "M. Leucker", TITLE = "Erf{\"u}llbarkeit globaler Spurlogiken mittels alternierender Automaten", BOOKTITLE = {9.~Theorietag der GI--Fachgruppe 0.1.5 ``Automaten und Formale Sprachen''}, EDITOR = {F.~Otto and G.~Niemann}, YEAR = {1999}, PUBLISHER = {University of Kassel}, SERIES = {Preprint}, VOLUME = {12/99}, PAGES = "46--47", } @INPROCEEDINGS{LL98, AUTHOR = "Martin Lange and Martin Leucker", TITLE = "Effizientes Spielbasiertes Model Checking f{\"u}r den Alternierungsfreien mu-Kalk{\"u}l", BOOKTITLE = {8.~Theorietag der GI--Fachgruppe 0.1.5 ``Automaten und Formale Sprachen''}, EDITOR = {H.~Seidl}, YEAR = {1998}, PUBLISHER = {University of Trier}, SERIES = {Forschungsbericht}, VOLUME = {98--17}, } @Book{Pnueli92, author = "Zohar Manna and Amir Pnueli", title = "The Temporal Logic of Reactive and Concurrent Systems", publisher = "Springer", address = "New York", year = "1992", descriptor = "Konkurrente Systeme, Reaktives System, Spezifikation, Temporale Logik", annote = "Buch ueber die Spezifikation von reaktiven Systemen in temporaler Logik. * Models of Concurrency: -Basic Models, -Modeling Real Concurrency * Specifications: -Temporal Logic, -Prosperties of Programs", } @Book{StandardML97, author = "Robin Milner and Mads Tofte and Robert Harper and David MacQueen", year = "1997", title = "The {Definition} of {Standard ML} (Revised)", publisher = "The MIT Press", } @Book{Thompson99, author = "Simon Thompson", title = "The Craft of Functional Programming", publisher = "Addison-Wesley", edition = "second", year = "1999", ISBN = "0-201-40357-9", abstract = "A textbook for beginners, learning Haskell as first programming language.", } @Book{Bird98, key = "Bird", author = "Richard J. Bird", title = "Introduction to Functional Programming using {Haskell}", edition = "second", publisher = "Prentice-Hall Europe", series = "Prentice-Hall Series in Computer Science", address = "London, UK", year = "1998", annote = "99 references.", } @Book{JavaLangSpec, title = "The {J}ava Language Specification", author = "James Gosling and Bill Joy and Guy Steele", publisher = "Addison-Wesley", series = "The {J}ava Series", ISBN = "0-201-63451-1", pages = "864", year = "1997", url = "http://java.sun.com/docs/books/jls/html/", } @InProceedings{MM96, author = "N.~Mart\'{i}--Oliet and J.~Meseguer", title = "Rewriting Logic as a Logical and Semantic Framework", booktitle = "First International Workshop on Rewriting Logic and its Applications", year = "1996", pages = "352--358", publisher = "Elsevier", series = "Electronic Notes in Theoretical Computer Science", volume = "4", } @InProceedings{Peled98, author = "Doron Peled", title = "Ten Years of Partial Order Reduction", booktitle = "Proceedings of 10th International Conference on Computer-Aided Verification (CAV'98)", series = "Lecture Notes in Computer Science", volume = "1427", publisher = "Springer", address = "Vancouver, BC, Canada", year = "1998", pages = "17--28", } @InProceedings{Gnesi, editor = "Susanne Graf and Michael Schwartzbach", author = "S. Gnesi and D. Latella and G. Lenzini and C. Abbaneo and A. Amendola and P. Marmo", title = "A Formal Specification and Validation of a Critical System in Presence of Byzantine Errors", booktitle = "Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems {(TACAS 2000)}", series = "Lecture Notes in Computer Science", number = "1785", publisher = "Springer", year = "2000", } @TechReport{VM00, author = "Alberto~Verdejo and Narcisco~Marti--Oliet", institution = "Universidad Complutense de Madrid", title = "Executing and Verifying CCS in Maude", number = "TR--SIP--99--00", publisher = "Depto.\ Sistemas Informaticos y Programacion", address = "Spain", month = feb, year = "2000", } @InProceedings{JaninW1996, title = "On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic", author = "David Janin and Igor Walukiewicz", pages = "263--277", booktitle = "CONCUR'96: Concurrency Theory, 7th International Conference", editor = "Ugo Montanari and Vladimiro Sassone", address = "Pisa, Italy", month = "26--29~" # aug, year = "1996", series = "Lecture Notes in Computer Science", volume = "1119", publisher = "Springer", ISBN = "ISBN 3-540-61604-7", URL = "http://www.brics.dk/~igw/concur96.ps", } @Article{EmeClarke82, author = "E. Allen Emerson and Edmund M. Clarke", title = "Using branching time temporal logic to synthesize synchronization skeletons", journal = "Science of Computer Programming", volume = "2", number = "3", pages = "241--266", month = dec, year = "1982", coden = "SCPGD4", ISSN = "0167-6423", keywords = "branching time temporal logic; concurrent programs; finite model property; mathematical programming; synchronization skeletons", } @Article{Andersen94, title = "Model checking and {Boolean} graphs", author = "Henrik Reif Andersen", journal = "Theoretical Computer Science", pages = "3--30", month = "11~" # apr, year = "1994", volume = "126", number = "1", } @Book{Papadimitriou94, author = "Christos H. Papadimitriou", title = "Computational Complexity", publisher = "Addison-Wesley", address = "New York", year = "1994", ISBN = "0-201-53082-1", keywords = "complexity, comutability, P, NP, coNP, NC, RNC, L, NL und PSPACE", } @Article{Reif:1985:DFS, author = "John H. Reif", title = "Depth-First Search is Inherently Sequential", journal = "Information Processing Letters", volume = "20", number = "5", pages = "229--234", day = "12", month = jun, year = "1985", coden = "IFPLAT", ISSN = "0020-0190", keywords = "adjacency lists; Algorithms; computational complexity; computer programming; depth-first search; deterministic log-space reductions; deterministic polynomial time; directed graphs; graph theory; mathematical techniques --- Graph Theory; parallel computation; parallel processing; polynomial time complete; rooted graph; sequential algorithms", } @Book{GHR95, author = "R. Greenlaw and H. J. Hoover and W. L. Ruzzo", title = "Limits to Parallel Computation: ${P}$-Completeness Theory", publisher = "Oxford University Press", year = "1995", } @Book{Reif93, author = "J. H. Reif", title = "Synthesis of Parallel Algorithms", publisher = "Morgan Kaufmann", address = "San Mateo", year = "1993", descriptor = "Parallele Berechnung, Paralleler Algorithmus", } @Book{Roosta99, author = "Seyed H. Roosta", title = "Parallel Processing and Parallel Algorithms", publisher = "Springer", address = "New York, Berlin, Heidelberg", year = "1999", ISBN = "0-387-98716-9", } @Article{Dijkstra:1980:TDD, author = "Edsger W. Dijkstra and C. S. Scholten", title = "Termination detection for diffusing computations", journal = "Information Processing Letters", volume = "11", number = "1", pages = "1--4", day = "29", month = aug, year = "1980", coden = "IFPLAT", ISSN = "0020-0190", mrclass = "68B05", mrnumber = "81h:68006", bibdate = "Wed Nov 11 12:16:26 MST 1998", acknowledgement = ack-nhfb, classification = "C4290 (Other computer theory)", corpsource = "Burroughs, Nuenen, Netherlands", keywords = "computation theory; computer metatheory; diffusing computations; graph; graph theory; messages; node; signalling scheme; termination detection", treatment = "T Theoretical or Mathematical", } @Book{Lester93, author = "Bruce P. Lester", title = "The Art of Parallel Programming", publisher = "Prentice Hall", year = 1993, } @Article{Zielonka87, author = "Wies{\l}aw Zielonka", journal = "R.A.I.R.O. --- Informatique {T}h{\'e}orique et Applications", pages = "99--135", title = "Notes on finite asynchronous automata", volume = "21", year = "1987", annote = "Finite asynchronous automata are introduced (only automata having such that for each action the reading and writing domains are equal are considered). It is proved that such automata recognize deterministically exactly all recognizable subsets of free partially commutative monoids. A subclass of asynchronous automata --- loosly cooperating automata --- is also introduced and examined. A special representation of recognizable sets of traces is deduced.", } @Book{Perry91, author = "D. Perry", title = "{VHDL}", publisher = "McGraw-Hill", address = "New York", year = "1991", descriptor = "HDL, VHDL", } @Book{Motorola93, editor = "Motorola", title = "The PowerPC (TM) 601 User's Manual", publisher = "Motorola", year = "1993", } @MastersThesis{Bollig00, author = "Benedikt Bollig", title = "Entwurf und {A}nalyse von {S}purlogiken", school = "Aachen, University of Technology", year = "2000", note = "(German)", postscript = PS # "bollig__diplomarbeit.ps.gz", } @MastersThesis{Hoefer00, author = "Thomas H{\"o}fer", title = "{Untersuchungen zum Einsatz boolescher Ausdruckdiagramme in der Verifikation}", school = "Aachen, University of Technology", year = "2000", note = "(German)", postscript = PS # "hoefer__diplomarbeit.ps.gz", } @TechReport{Maz77, author = "Antoni Mazurkiewicz", address = "Aarhus", institution = "Aarhus University", number = "78", title = "Concurrent Program Schemes and their Interpretations", type = "{DAIMI Rep. PB}", year = "1977", annote = "The classical technical report which introduced the notion of trace. Traces are shown to be an adequate partial order semantics for concurrent programs. In particular, the semantics of elementary net systems can be adequately described using traces. Traces are represented as labelled partial orders or dependence graphs.", } @PhdThesis{Kamp68, address = "Los Angeles", author = "H. W. Kamp", key = "Kamp68", keyword = "omega", school = "University of California", title = "Tense Logic and the Theory of Linear Order", year = "1968", } @InProceedings{DiekertGastin00, author = "Volker Diekert and Paul Gastin", editor = "F. Orejas and P. G. Spirakis and J. van Leeuwen", title = "{LTL} is expressively complete for {M}azurkiewicz traces", booktitle = "Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000)", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1853", year = "2000", pages = "211--222", } @TechReport{Walukiewicz2000, author = "Igor Walukiewicz", title = "Local Logics for Traces", institution = "BRICS", year = "2000", number = "RS-00-2", url = "http://www.brics.dk/~igw/igw-trace-local.ps", } @InProceedings{Walu96, address = "New Brunswick, NJ, USA", author = "I. Walukiewicz", booktitle = "Proceedings of the Eighth International Conference on Computer-Aided Verification (CAV'96)", editor = "Rajeev Alur and Thomas A. Henzinger", key = "Walu96", month = jul # "/" # aug, pages = "62--74", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Pushdown Processes: Games and Model Checking", volume = "1102", year = "1996", } @InProceedings{cade97*191, author = "Moshe Y. Vardi", title = "Alternating Automata: Unifying Truth and Validity Checking for Temporal Logics", pages = "191--206", ISBN = "3-540-63104-6", editor = "William McCune", booktitle = "Proceedings of the 14th International Conference on Automated deduction", month = jul # "~13--17", series = "LNAI", volume = "1249", publisher = "Springer", address = "Berlin", year = "1997", url = "http://www.cs.rice.edu/~vardi/papers/cade97.ps.gz", } @TechReport{Thiagarajan95b, author = "P. S. Thiagarajan", title = "{PTL} over Product State Spaces", institution = "School of Mathematics, SPIC Science Foundation", year = "1995", number = "TCS-95-4", } @Article{Sewell:1998:RRB, author = "P. Sewell", title = "From Rewrite Rules to Bisimulation Congruences", journal = "Lecture Notes in Computer Science", volume = "1466", pages = "269--??", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", } @InProceedings{Reffel99, author = "Reffel", title = "{BDD}-Nodes Can Be More Expressive", booktitle = "ACSC: Asian Computing Science Conference, LNCS", year = "1999", } @InCollection{Nadathur98handbook, author = "Gopalan Nadathur and Dale Miller", title = "Higher-Order Logic Programming", booktitle = "Handbook of Logic in Artificial Intelligence and Logic Programming", publisher = "Oxford University Press", year = "1998", editor = "D. M. Gabbay and C. J. Hogger and J. A. Robinson", volume = "5", chapter = "8", keywords = "lambda-Prolog", } @Unpublished{Mukund97, author = "Madhavan Mukund", title = "Linear-Time Temporal Logic and {B}{\"u}chi Automata", note = "Tutoriala talk, Winter School on Logic and Computer Science", month = jan, year = "1997", url = "http://www.smi.ernet.in/~madhavan/papers/isical97.html", } @PhdThesis{Mader96, author = "Angelika Mader", title = "Verification of Modal Properties Using Boolean Equation Systems", school = "Technische {Universit\"at} {M\"unchen}", year = "1996", } @article{Lechner96a, author = {U.~Lechner}, title = {Object-Oriented Specifications of Distributed Systems in the $\mu$-Calculus and {Maude}}, journal = {Electronic Notes in Theoretical Computer Science}, volume = {4}, year = 1996, note = {Proc. First International Workshop on Rewriting Logics and its applications.} } @Article{Launchbury:1995:SH, author = "John Launchbury and Simon L. {Peyton Jones}", title = "State in {Haskell}", journal = "Lisp and Symbolic Computation", volume = "8", number = "4", pages = "293--341", month = dec, year = "1995", coden = "LSCOEX", ISSN = "0892-4635", bibdate = "Fri Feb 12 08:11:22 MST 1999", url = "http://www.wkap.nl/oasis.htm/97403", acknowledgement = ack-nhfb, affiliation = "Oregon Graduate Inst", affiliationaddress = "Portland, USA", classification = "721.1; 723.1; 723.1.1; 902.2", journalabr = "LISP Symb Comput", keywords = "Algorithms; Computation theory; Computer programming; Computer programming languages; Functional programming; Input output programs; Parametricity; Side-effects; Specifications; Types", } @InProceedings{STOC98*224, author = "Orna Kupferman and Moshe Y. Vardi", title = "Weak Alternating Automata and Tree Automata Emptiness", pages = "224--233", ISBN = "0-89791-962-9", booktitle = "Proceedings of the 30th Annual {ACM} Symposium on Theory of Computing ({STOC}-98)", month = may # "~23--26", publisher = "ACM Press", address = "New York", year = "1998", } @TechReport{Husson99, author = "J.-F. Husson and R. Morin", title = "Relationships between Arnold's CCI sets of P-traces and Droste's concurrent automata", institution = "IRIT, Universite Paul Sabatier, Tolouse, France", year = "1999", } @TechReport{Henriksen99, author = "Jesper Henriksen", title = "An Expressive Extension of {TLC}", institution = "BRICS", year = "1999", number = "RS-99-26", month = sep, url = "http://www.brics.dk/RS/99/26/", } @InProceedings{Al99a, author = "R. Alur and M. Yannakakis", title = "Model Checking of Message Sequence Charts", booktitle = "Proceedings of the 10th International Conference on Concurrency Theory", pages = "114--129", publisher = "Springer", year = "1999", series = "Lecture Notes in Computer Science", volume = "1664", url = "http://www.cis.upenn.edu/~alur/Concur99msc.ps.gz", } @Article{Alechina00, author = "N. Alechina and N. Immerman", title = "Reachability Logic: An Efficient Fragment of Transitive Closure Logic", journal = "Logic Journal of the IGPL", year = "2000", volume = "8", number = "3", pages = "325--338", url = "http://www.cs.umass.edu/~immerman/pub/efficient.ps", } @Book{KemperEickler99, Author = {Alfons Kemper and Andr{\'e} Eickler}, Title = {Datenbanksysteme}, Year = {1999}, Publisher = {R. Oldenbourg Verlag} } @Book{Vossen99, Author = {Gottfried Vossen}, Title = {Datenbankmodelle, Datenbanksprachen und Datenbankmanagement-Systeme}, Year = {1999}, Publisher = {R. Oldenbourg Verlag} } @TechReport{IB-B921106, author = "P. Gastin and A. Petit", title = "Asynchronous Automata for Infinite Traces", institution = "LSV, ENS de Cachan", address = "Orsay", year = "1991", descriptor = "Automatentheorie, Infinite Traces, Prozess-Theorie, Trace Theory", annote = "Bericht 707, LRI, Univ. Paris-Sud, Orsay: Es wird die Charakterisierung von nichtbeschraenktem Verhalten durch asynchrone parallele Automaten beschrieben.", } @InProceedings{ICALP::GastinP1992, title = "Asynchronous Cellular Automata for Infinite Traces", author = "Paul Gastin and Antoine Petit", editor = "Werner Kuich", booktitle = "Automata, Languages and Programming, 19th International Colloquium", address = "Vienna, Austria", month = "13--17~" # jul, year = "1992", series = "Lecture Notes in Computer Science", volume = "623", publisher = "Springer", pages = "583--594", } @InCollection{gp95, author = "Paul Gastin and Antoine Petit", title = "Infinite traces", booktitle = "The Book of Traces", chapter = "11", editor = "V. Diekert and G. Rozenberg", publisher = "World Scientific", address = "Singapore", year = "1995", pages = "393--486", } @InCollection{dm96handbook, author = "Volker Diekert and Yves M{\'e}tivier", address = "Berlin-Heidelberg-New York", booktitle = "Handbook on Formal Languages", editor = "G. Rozenberg and A. Salomaa", publisher = "Springer", title = "Partial Commutation and Traces", volume = "III", year = "1997", } @InProceedings{LeuckerBaader98, author = "F. Baader and M. Leucker", title = "Comparison of two Semantic Approaches to Unification", booktitle = "Proceedings of the 12th International Workshop on Unification", year = "1998", number = "SI-98/8", series = "Research Report", address = "Universita di Roma, La Sapienza", month = jun, url = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker_baader__unif98.ps.gz", postscript = Documents # "Leucker/unif98.ps.gz", } @Article{Milner:1983:CSA, author = "R. Milner", title = "Calculi for synchrony and asynchrony", journal = "Theoretical Computer Science", volume = "25", number = "3", pages = "267--310", month = jul, year = "1983", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Sat Nov 22 13:36:07 MST 1997", acknowledgement = ack-nhfb, classification = "C4230B (Combinatorial switching theory)", corpsource = "Dept. of Computer Sci., Edinburgh Univ., Edinburgh, UK", keywords = "Abelian group; algebraic theory; asynchrony; bisimulation; calculus; combinatorial switching; combinators; distributed computation; modelling; synchrony", pubcountry = "Netherlands", treatment = "T Theoretical or Mathematical", } @InProceedings{CaspiEtAl87, author = "P. Caspi and D. Pilaud and N. Halbwachs and J. A. Plaice", title = "{LUSTRE}: {A} Declarative Language for Programming Synchronous Systems", booktitle = "Conference Record of the Fourteenth Annual {ACM} Symposium on Principles of Programming Languages", address = "Munich, West Germany", organization = "ACM SIGACT-SIGPLAN", publisher = "ACM Press", month = jan # " 21--23,", year = "1987", pages = "178--188", } @InProceedings{Bensalem99:DCCA, title = "A Methodology for Proving Control Systems with {Lustre} and {PVS}", author = "S. Bensalem and P. Caspi and C. Parent-Vigouroux and C. Dumas", booktitle = "Dependable Computing for Critical Applications---7", editor = "Charles B. Weinstock and John Rushby", pages = "89--107", publisher = "IEEE Computer Society Press", series = "Dependable Computing and Fault Tolerant Systems", volume = "12", month = jan, year = "1999", address = "San Jose, CA", } @InProceedings{Leucker00, author = "Martin Leucker", title = "Parallel Model Checking for the Alternation-Free Mu-Calculus", booktitle = "FM-TOOLS 2000, The 4th Workshop on Tools for System Design and Verification", pages = "135--140", year = "2000", editor = "Gerhard Schellhorn and Wolfgang Reif", volume = "2000-07", month = may, publisher = "Ulmer Informatik Berichte", note = "Extended Abstract", seealso = "BLW02", } @InProceedings{LeuckerNoll00, author = "Martin Leucker and Thomas Noll", title = "Rewriting Logic as a Framework for Generic Verification Tools", booktitle = "Proceedings of the Third International Workshop on Rewriting Logic and its Applications (WRLA'00)", year = "2000", Teditor = "Kokichi Futatsugi", volume = "36", series = "Electronic Notes in Theoretical Computer Science", publisher = "Elsevier", url = "http://www.elsevier.nl/gej-ng/31/29/23/71/22/show/Products/notes/index.htt", } @InProceedings{LeuckerNollb00, author = "Martin Leucker and Thomas Noll", title = "Truth - {A} Real-World Application in {H}askell", booktitle = "Proceedings of the 12th International Workshop on Implementation of Functional Languages (IFL'00)", pages = "363--380", year = "2000", editor = "Markus Mohnen", number = "AIB-00-7", series = "Aachener Informatik Berichte", month = sep, organization = "RWTH Aachen", url = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker__Truth_Haskell.ps.gz", postscript = Documents # "Leucker/Truth_Haskell.ps.gz", } @INPROCEEDINGS{SD97, AUTHOR = "U. Stern and D. L. Dill", TITLE = "Parallelizing the {Mur$\varphi$} Verifier", BOOKTITLE = "Computer-Aided Verification, 9th International Conference", Editor = "Orna Grumberg", Series="Lecture Notes in Computer Science", Volume="1254", Publisher="Springer", MONTH = "June", YEAR = "1997", PAGES = "256--267", NOTE = "Haifa, Israel, June 22-25", url = "http://sprout.stanford.edu/PAPERS/SD97.ps", } @inproceedings{HYD94, title = "New Techniques for Efficient Verification with Implicitly Conjoined {BDDs}", author = "Alan J. Hu and Gary York and David L. Dill", booktitle = "31st Design Automation Conference", pages="276--282", year = "1994", url = "http://sprout.stanford.edu/PAPERS/HYD94.ps", } @MastersThesis{Basonov98, author = "S. Basonov", title = "Parallel Implementation of {BDD} on {DSM} Systems", school = "Computer Science Department, Technion", year = "1998", } @InProceedings{Cabodi96, author = "Gianpiero Cabodi and Paolo Camurati and Stefano Que", title = "Improved reachability analysis of large {FSM}", booktitle = "Proceedings of the {IEEE} International Conference on Computer-Aided Design", Publisher = "{IEEE} Computer Society Press", month = jun, year = "1996", pages = "354--360", } @InProceedings{Narayan97, author = "Adrian A. Narayan and Jain J. Jawahar Isles and Robert K. Brayton and Alberto L. Sangiovanni-Vincentelli", title = "Reachability analysis using partitioned--{roBBDs}", booktitle = "Proceedings of the {IEEE} International Conference on Computer-Aided Design", Publisher = "{IEEE} Computer Society Press", month = jun, year = "1997", pages = "388--393", } @InProceedings{Narayan96, author = "Adrian A. Narayan and Jain J. Jawahar Isles and M. Fujita and Alberto L. Sangiovanni-Vincentelli", title = "Partitioned--{roBBDs}", booktitle = "Proceedings of the {IEEE} International Conference on Computer-Aided Design", Publisher = "{IEEE} Computer Society Press", month = jun, year = "1996", pages = "547--554", } @INPROCEEDINGS{Heyman00, AUTHOR = "Tamir Heyman and Danny Geist and Orna Grumberg and Assaf Schuster", TITLE = "Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits", BOOKTITLE = "Computer-Aided Verification, 12th International Conference", Editor = "Orna Grumberg", Series="Lecture Notes in Computer Science", Volume="1855", Publisher="Springer", MONTH = "June", YEAR = "2000", PAGES = "20--35", url = "http://www.cs.technion.ac.il/~tamirh/parsmv_cav00.ps", } @InProceedings{buc62, author = "J. R. B{\"u}chi", title = "On a Decision Method in Restricted Second Order Arithmetic", pages = "1--12", booktitle = "Proceedings of the International Congress on Logic, Method, and Philosophy of Science", year = "1962", publisher = "Stanford University Press", address = "Stanford, CA, USA", } @InProceedings{LoedingThomas00, author = "C. L{\"o}ding and W. Thomas", title = "Alternating Automata and Logics over Infinite Words", booktitle = "Proceedings of the IFIP International Conference on Theoretical Computer Science, IFIP TCS2000", pages = "521-535", year = 2000, volume = "1872", series = "Lecture Notes in Computer Science", month = aug, publisher = "Springer", url = "http://www-i7.informatik.rwth-aachen.de/~loeding/ifiptcs2000.ps.gz", } @InProceedings{Leucker00b, title ="On model checking synchronised hardware circuits", author ="Martin Leucker", editor ="Jifeng He and Masahiko Sato", booktitle ="Proceedings of the 6th Asian Computing Science Conference ({ASIAN'00})", pages ="182--198", address ="Penang, Malaysia", year =2000, month =nov, publisher ="Springer", series ="Lecture Notes in Computer Science", volume ="1961", url ="http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/leucker__foata.ps.gz", postscript = Documents # "Leucker/foata.ps.gz", } @INPROCEEDINGS{BHL00a, AUTHOR = "B. Bollig and J. Henriksen and M. Leucker", TITLE = "Deciding {LTL} over {M}azurkiewicz Traces", BOOKTITLE = {Theorietag 2000 mit Workshop ``New Computing Paradigms: Molecular Computing and Quantum Computing''}, EDITOR = {R. Freund}, YEAR = 2000, PUBLISHER = "Vienna University of Technology", PAGES = "167--174", ISBN = {3-85028-325-9}, url = "http://www-i2.informatik.rwth-aachen.de/leucker/Literatur/Ps_files/BHL__vienna00_paper.ps.gz", postscript = PS # "BHL__vienna00_paper.ps.gz", } @Article{KVW00, author = "Orna Kupferman and Moshe Y. Vardi and Pierre Wolper", title = "An automata-theoretic approach to branching-time model checking", journal = "Journal of the ACM", volume = "47", number = "2", pages = "312--360", month = mar, year = "2000", coden = "JACOAH", ISSN = "0004-5411", bibdate = "Wed Sep 20 16:53:37 MDT 2000", url = "http://www.acm.org/pubs/citations/journals/jacm/2000-47-2/p312-kupferman/", abstract = "Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper, we show that {\em alternating tree automata\/} are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only can they be used to obtain optimal decision procedures, as was shown by Muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.", acknowledgement = ack-nhfb, keywords = "algorithms; verification", subject = "Theory of Computation --- Analysis of Algorithms and Problem Complexity --- Nonnumerical Algorithms and Problems (F.2.2): {\bf Computations on discrete structures}; Mathematics of Computing --- Discrete Mathematics --- Graph Theory (G.2.2); Mathematics of Computing --- Discrete Mathematics --- Graph Theory (G.2.2): {\bf Graph algorithms}", annote = "Full version of CAV'94 paper", } @Article{Courcoubetis:1991:MEA, author = "Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper and Mihalis Yannakakis", title = "Memory Efficient Algorithms for the Verification of Temporal Properties", journal = "Lecture Notes in Computer Science", volume = "531", pages = "233--??", year = "1991", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Mon May 13 08:51:55 MDT 1996", acknowledgement = ack-nhfb, } @InProceedings{Pnueli77, author = "Amir Pnueli", title = "The temporal logic of programs", booktitle = "Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS-77)", address = "Providence, Rhode Island", publisher = "IEEE Computer Society Press", month = oct # " 31--" # nov # " 2", year = "1977", pages = "46--57", annote = "Presents the idea of reactive systems and temporal logic in contrast to transformationel systems using Hoare Logic.", } @InProceedings{BLW01, author = "Benedikt Bollig and Martin Leucker and Michael Weber", title = "Parallel Model Checking for the Alternation Free $\mu$-Calculus", booktitle = "Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)", pages = "543--558", year = "2001", editor = "Tiziana Margaria and Wang Yi", volume = 2031, series = "Lecture Notes in Computer Science", month = apr, publisher = "Springer", seealso = "BLW02", } @InProceedings{LICS::ZhangSS1994, title = "On the Parallel Complexity of Model Checking in the Modal Mu-Calculus", author = "Shipei Zhang and Oleg Sokolsky and Scott A. Smolka", pages = "154--163", booktitle = "Proceedings of the 9th Annual {IEEE} Symposium on Logic in Computer Science", year = 1994, month = "4--7 " # jul, address = "Paris, France", organization = "IEEE Computer Society Press", references = "\cite{JACM::AfratiP1993} \cite{LICS::EmersonL1986} \cite{JACM::HennessyM1985} \cite{IC::KanellakisS1990}", } @Article{Dijkstra:1983:DTD, author = "Edsger W. Dijkstra and W. H. J. Feijen and A. J. M. {van Gasteren}", title = "Derivation of a Termination Detection Algorithm for Distributed Computations", journal = "Information Processing Letters", volume = "16", number = "5", pages = "217--219", day = "10", month = jun, year = "1983", coden = "IFPLAT", ISSN = "0020-0190", mrclass = "68B05 (68C05)", mrnumber = "84m:68005", bibdate = "Wed Nov 11 12:16:26 MST 1998", acknowledgement = ack-nhfb, classification = "723; B6210L (Computer communications); C5620 (Computer networks and techniques); C6150J (Operating systems)", corpsource = "Burroughs, AL Nuenen, Netherlands", journalabr = "Inf Process Lett", keywords = "computer programming; distributed computations; distributed processing; networks; protocols; termination detection algorithm", treatment = "P Practical", } @PhdThesis{Rohde97, author = "S. Rohde", title = "Alternating automata and the temporal logic of ordinals", school = "University of Illinois at Urbana-Champaign", year = "1997", } @InProceedings{Valmari90, author = "Antti Valmari", title = "A Stubborn Attack On State Explosion", pages = "156--165", ISBN = "3-540-54477-1", editor = "Edmund M. Clarke and Robert P. Kurshan", booktitle = "Proceedings of Computer-Aided Verification ({CAV}'90)", month = jun, series = "Lecture Notes in Computer Science", volume = "531", publisher = "Springer", address = "Berlin, Germany", year = "1991", } @InProceedings{Thiagarajan94, title = "A Trace Based Extension of Linear Time Temporal Logic", author = "P. S. Thiagarajan", pages = "438--447", booktitle = "Proceedings, Ninth Annual {IEEE} Symposium on Logic in Computer Science", year = "1994", month = "4--7 " # jul, address = "Paris, France", organization = "IEEE Computer Society Press", references = "\cite{IC::LodayaPRT1995} \cite{FOCS::Pnueli1977} \cite{JACM::SistlaC1985} \cite{LICS::VardiW1986}", } @InProceedings{EbingerMuscholl93, author = "Werner Ebinger and Anca Muscholl", booktitle = "Proceedings of the 20th International Colloquium on Automata, Languages and Programming (ICALP'93)", address = "Lund, Sweden", editor = "A. Lingas and R. Karlsson and S. Carlsson", volume = "700", pages = "335--346", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Logical definability on infinite traces", year = "1993", annote = "The equivalence of monadic second order definability and recognizability and the equivalence of first order definability, star-freeness, and aperiodicity are generalized to languages of infinite traces.", } @Article{EbingerMuscholl96, author = "Werner Ebinger and Anca Muscholl", title = "Logical definability on infinite traces", journal = "Theoretical Computer Science", volume = "154", number = "1", pages = "67--84", day = "22", month = jan, year = "1996", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Mon Jul 19 22:19:40 MDT 1999", url = "http://www.elsevier.com/cgi-bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?year=1996&;volume=154&issue=1&aid=2071", acknowledgement = ack-nhfb, classification = "C4210 (Formal logic); C4210L (Formal languages and computational linguistics)", conflocation = "Lund, Sweden; 5-9 July 1993", conftitle = "Proceedings of the 20th International Colloquium on Automata, Languages and Programming (ICALP'93)", corpsource = "Inst. f{\"u}r Inf., Stuttgart Univ., Germany", keywords = "aperiodic real trace language; computation theory; computational linguistics; definability; equivalence; finite trace; first-order definable trace language; formal logic; infinite trace; infinite traces; infinite words; logic; logical definability; monadic second-order logic; real trace language; recognizability; recognizable language characterization; star-free trace language", pubcountry = "Netherlands", treatment = "T Theoretical or Mathematical", } @Unpublished{Caucal01, author = "Didier Caucal", title = "On the transition graphs of turing machines", note = "Unpublished", month = jan, year = 2001, } @InProceedings{Caucal96, author = "Didier Caucal", address = "Berlin-Heidelberg-New York", booktitle = "Proceedings of the 23th International Colloquium on Automata, Languages and Programming (ICALP'96)", editor = "F. Meyer auf der Heide and B. Monien", volume = "1099", pages = "194--205", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "On infinite transition graphs having a decidable monadic theory", year = "1996", annote = "full version to appear in TCS", } @Book{clarke_em-etal:1999a, author = "Edmund M. Clarke and Orna Grumberg and Doron A. Peled", title = "Model Checking", publisher = "The {MIT} Press", year = "1999", address = "Cambridge, Massachusetts", ISBN = "0262032708", topic = "model-checking;program-verification;", } @Article{Buechi:60, author = "J. B{\"u}chi", title = "Weak Second Order Logic and Finite Automata", journal = "Z. Math. Logik, Grundlag. Math.", volume = "5", pages = "66--62", year = "1960", added = "1996-03-13-10-09-20", } @Article{Rabin:69, author = "M. O. Rabin", title = "Decidability of Second-Order Theories and Automata on Infitite Trees", journal = "Trans. of Amer. Math. Soc.", volume = "141", pages = "1--35", year = "1969", added = "1996-03-13-10-09-20", } @Article{Muller:1985:TEP, author = "D. E. Muller and P. E. Schupp", title = "The theory of ends, pushdown automata, and second-order logic", journal = "Theoretical Computer Science", volume = "37", number = "1", pages = "51--75", month = may, year = "1985", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Sat Nov 22 13:29:49 MST 1997", acknowledgement = ack-nhfb, classification = "C1160 (Combinatorial mathematics); C4210 (Formal logic); C4220 (Automata theory)", corpsource = "Dept. of Math., Comput. Sci. Illinois Univ., Urbana, IL, USA", keywords = "automata theory; Cayley graphs; cellular automata; context free groups; edge-labeled graphs; ends theory; formal logic; graph theory; infinite binary tree; monadic second-order theory; pushdown automata; Rabin's theorem; second-order logic theory; tiling systems; trees (mathematics); two dimensional grid", pubcountry = "Netherlands A03", treatment = "T Theoretical or Mathematical", } @InProceedings{Barthelmann:1998:WCE, author = "K. Barthelmann", booktitle = "MFCS: Symposium on Mathematical Foundations of Computer Science", title = "When Can an Equational Simple Graph Be Generated by Hyperedge Replacement?", series = "Lecture Notes in Computer Science", volume = "1450", pages = "543--??", year = "1998", coden = "LNCSD9", } @InCollection{Tho97handbook, author = "W. Thomas", title = "Languages, Automata and Logic", booktitle = "Handbook of Formal Languages", publisher = "Springer", address = "Berlin", year = "1997", editor = "A. Salomaa and G. Rozenberg", volume = "3, Beyond Words", } @Article{Cou95b, author = "B. Courcelle", title = "The monadic second order logic of graphs {IX}: machine and their behaviours", journal = "Theoretical Comput. Sci.", volume = "151", year = "1995", pages = "125--162", } @Unpublished{Stirling00, author = "Colin Stirling", title = "Decidability of Bisimulation Equivalence for Pushdown Processes", note = "Unpublished", OPTkey = {}, OPTmonth = {}, year = "2000", OPTannote = {} } @TechReport{mscitu96, author = "ITU-TS", title = "{ITU-TS Recommendation Z.120: Message Sequence Chart 1996 (MSC96)}", institution = "ITU-TS, Geneva", year = "1996", } @TechReport{mscituannex98, author = "ITU-TS", title = "{ITU-TS Recommendation Z.120anb: Formal Semantics of Message Sequence Charts}", institution = "ITU-TS, Geneva", year = "1998", } @TechReport{mscitu99, author = "ITU-TS", title = "{ITU-TS Recommendation Z.120: Message Sequence Chart 1999 (MSC99)}", institution = "ITU-TS, Geneva", year = "1999", } @InProceedings{Ramanujam00, author = "B. Meenakshi and R. Ramanujam", title = "Reasoning about message passing in finite state environments", booktitle = "Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000)", editor = "F. Orejas and P. G. Spirakis and J. van Leeuwen", publisher = "Springer", series = "Lecture Notes in Computer Science", year = "2000", volume = "1853", } @InProceedings{Henriksen00b, author = "J. G. Henriksen and M. Mukund and K. Narayan Kumar and P. S. Thiagarajan", title = "On Message Sequence Graphs and Finitely Generated Regular MSC Languages", booktitle = "Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000)", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1853", year = "2000", pages = "675--686", } @InProceedings{Henriksen00a, author = "J. G. Henriksen and M. Mukund and K. Narayan Kumar and P. S. Thiagarajan", title = "Regular Collections of Message Sequence Charts", booktitle = "Proceedings of 25th International Symposium on Mathematical Foundations of Computer Science (MFCS'2000)", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1893", year = "2000", pages = "405--414", } @InProceedings{Araujo:1998:OOPSLAWS, author = "Jo{\~a}o Ara{\'u}jo", title = "Formalizing Sequence Diagrams", booktitle = "Proceedings of the OOPSLA'98 Workshop on Formalizing UML. Why? How?", editor = "Luis Andrade and Ana Moreira and Akash Deshpande and Stuart Kent", year = "1998", series = "ACM SIGPLAN Notices", volume = "33, 10", publisher = "ACM Press", address = "New York", } @Article{Lamport:1978:TCO, author = "Leslie Lamport", title = "Time, Clocks, and the Ordering of Events in a Distributed System", journal = "Communications of the ACM", volume = "21", number = "7", pages = "558--565", month = jul, year = "1978", coden = "CACMA2", ISSN = "0001-0782", bibdate = "Tue Mar 25 13:26:09 MST 1997", abstract = "The concept of one event happening before another in a distributed system is examined, and is shown to define a partial ordering of the events. A distributed algorithm is given for synchronizing a system of logical clocks which can be used to totally order the events. The use of the total ordering is illustrated with a method for solving synchronization problems. The algorithm is then specialized for synchronizing physical clocks, and a bound is derived on how far out of synchrony the clocks can become.", acknowledgement = ack-nhfb, annote = "Classic paper on logical clocks. A classic paper on synchronization. Reproduced in ``Distributed Computing: Concepts and Implementations'' edited by McEntire, O'Reilly and Larson, IEEE, 1984. The concept of one event happening before another in a distributed system is examined, and is shown to define a partial ordering of the events. A distributed algorithm is given for synchronising a system of logical clocks which can be used to totally order the events. The use of the total ordering is illustrated with a method for solving synchronisation problems. The algorithm is then specialised for synchronising physical clocks, and a bound is derived on how far out of synchrony the clocks can become.", classcodes = "C6150J (Operating systems)", classification = "723", journalabr = "Commun ACM", keywords = "5.29 distributed processing computer networks multiprocessing programs ordering of events distributed system synchronising total ordering clocks computer networks multiprocessing bsatya enm; clock synchronization; clocks; computer networks; computer operating systems; distributed computer systems; distributed processing; distributed system; distributed systems; dmp; grecommended91 CR categories: 4.32; jw; multiprocess systems; multiprocessing; ordering; ordering of events; programs; synchronising; total", treatment = "T Theoretical or Mathematical", } @InCollection{Lamport-Lynch90, author = "Leslie Lamport and Nancy Lynch", booktitle = "Handbook of Theoretical Computer Science", title = "Distributed Computing: Models and Methods", chapter = "19", publisher = "The MIT Press", year = "1990", editor = "J. van Leewen", pages = "1157--1199", volume = "B: Formal Models and Semantics", address = "New York, NY", annote = "81 references.", } @TechReport{BolligLeucker01, author = "Benedikt Bollig and Martin Leucker", title = "Deciding {LTL} over {M}azurkiewicz traces", institution = "RWTH Aachen", year = "2001", number = "AIB-02-2001", month = feb, postscript= PS # "bollig_leucker__deciding_ltl.ps.gz", url = PS # "bollig_leucker__deciding_ltl.ps.gz", } @InProceedings{KupVar00, author = "Orna Kupferman and Moshe Y. Vardi", title = "An Automata-Theoretic Approach to Reasoning about Infinite-State Systems", booktitle = "Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00)", editor = "E. A. Emerson and A. P. Sistla", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1855", year = "2000", } @InProceedings{AEY2000, author = "R. Alur and K. Etessami and M. Yannakakis", title = "Inference of Message Sequence Charts", booktitle = "22nd International Conference on Software Engineering", year = "2000", pages = "304--313", url = "http://www.cis.upenn.edu/~alur/Icse00.ps.gz", } @InProceedings{LeuckerNoll01, author = "Martin Leucker and Thomas Noll", title = "Truth/{SLC} - {A} Parallel Verification Platform for Concurrent Systems", booktitle = "Proceedings of the 13th Conference on Computer-Aided Verification (CAV'01)", pages = "255--259", year = "2001", editor = "G\'erard Berry and Hubert Comon and Alain Finkel", volume = "2102", series = "Lecture Notes in Computer Science", month = jul, publisher = "Springer", url = PS # "leucker_noll__TruthSLC.ps.gz", postscript = Documents # "Leucker/TruthSLC.ps.gz", } @TechReport{BolligLeuckerWeber01, author = "Benedikt Bollig and Martin Leucker and Michael Weber", title = "Local Parallel Model Checking for the Alternation Free $\mu$--Calculus", institution = "RWTH Aachen", year = "2001", number = "AIB-04-2001", month = mar, url = "http://aib.informatik.rwth-aachen.de/2001/2001-04.ps.gz", postscript = Documents # "Leucker/2001-04.ps.gz", } @InProceedings{BolligLeucker01a, author = "Benedikt Bollig and Martin Leucker", title = "Deciding {LTL} over {M}azurkiewicz Traces", booktitle = "Proceedings of the Symposium on Temporal Representation and Reasoning {(TIME'01)}", pages = "189--197", year = "2001", editor = "Claudio Bettini and Angelo Montanari", month = jun, publisher = "IEEE Computer Society Press", postscript= PS # "bollig_leucker__deciding_ltl.ps.gz", url = PS # "bollig_leucker__deciding_ltl.ps.gz", } @InProceedings{BolligLeucker01b, author = "Benedikt Bollig and Martin Leucker", title = "Modelling, {S}pecifying, and {V}erifying {M}essage {P}assing {S}ystems", booktitle = "Proceedings of the Symposium on Temporal Representation and Reasoning {(TIME'01)}", pages = "240--248", year = "2001", editor = "Claudio Bettini and Angelo Montanari", month = jun, publisher = "IEEE Computer Society Press", postscript= PS # "bollig_leucker__MPS_ext.ps.gz", url = PS # "bollig_leucker__MPS_ext.ps.gz", } @TechReport{BolligLeuckerNoll01, author = "Benedikt Bollig and Martin Leucker and Thomas Noll", title = "Regular {MSC} {L}anguages", institution = "RWTH Aachen", year = "2001", number = "AIB-05-2001", month = apr, postscript = PS # "bollig_leucker_noll__regular_msc.ps.gz", url = "http://aib.informatik.rwth-aachen.de/2001/2001-05.ps.gz", } @TechReport{BolligLeuckerNoll02, author = "Benedikt Bollig and Martin Leucker and Thomas Noll", title = "Generalised {R}egular {MSC} {L}anguages", institution = "RWTH Aachen", year = "2002", number = "AIB-03-2002", month = jan, url = "http://aib.informatik.rwth-aachen.de/2002/2002-03.ps.gz", postscript = Documents # "Leucker/2002-03.ps.gz", } @InProceedings{BurkartS92, title = "Model Checking for Context-Free Processes", author = "Olaf Burkart and Bernhard Steffen", pages = "123--137", booktitle = "CONCUR'92: Third International Conference on Concurrency Theory", editor = "W. R. Cleaveland", address = "Stony Brook, New York", month = "24--27" # aug, year = "1992", series = "Lecture Notes in Computer Science", volume = "630", publisher = "Springer", ISBN = "ISBN 3-540-55822-5 and 0-387-55822-5", } @Booklet{Caucal98, title = "Sur des graphs infinis r{\'e}guliers", author = "Didier Caucal", address = "IRISA -- IFSIC", year = "1998", note = "Documents d'habilitation", } @TechReport{Blumensath01, author = "Achim Blumensath", title = "Prefix-Recognizable Graphs and Monadic Second Order Logic", institution = "RWTH Aachen", year = "2001", number = "AIB-06-2001", month = apr, url = "http://aib.informatik.rwth-aachen.de/2001/2001-06.ps.gz", } @Article{Caucal01b, author = "Didier Caucal", title = "On infinite transition graphs having a decidable monadic theory", journal = "Theoretical Computer Science", year = "2001", note = "to appear" } @Misc{Truth, key = "Truth", title = "The \textsc{Truth} Verification Tool", note = "\url{http://www-i2.informatik.rwth-aachen.de/Research/MCS/Truth}" } @MastersThesis{Weber01, author = "Michael Weber", title = "{P}aralleles {M}odel {C}hecking", school = "Aachen, University of Technology", year = "2001", note = "(German)", postscript = PS # "weber__diplomarbeit.ps.gz", pdf = PS # "weber__diplomarbeit.pdf.gz", } @InProceedings{NevenSV01, author = {Frank Neven and Thomas Schwentick and Victor Vianu}, title = {Towards regular languages over infinite alphabets}, booktitle = "Proceedings of 26th International Symposium on Mathematical Foundations of Computer Science (MFCS'01)", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "", year = "2001", } @Article{Kaminski:1994:FMA, author = "Michael Kaminski and Nissim Francez", title = "Finite-memory automata", journal = "Theoretical Computer Science", volume = "134", number = "2", pages = "329--363", day = "21", month = nov, year = "1994", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Mon Jul 19 22:18:34 MDT 1999", url = "http://www.elsevier.com/cgi-bin/cas/tree/store/tcs/cas_sub/browse/browse.cgi?year=1994&;volume=134&issue=2&aid=1631", classification = "C4210 (Formal logic); C4220 (Automata theory)", corpsource = "Dept. of Comput. Sci., Hong Kong Univ. of Sci. and Technol., Kowloon, Hong Kong", keywords = "classical Rabin-Scott finite-state automata; closure; computation model; decidability; decision properties; equality test; finite alphabets; finite automata; finite-memory automata; finite-state automata; generalization; infinite alphabets; substitution", pubcountry = "Netherlands", } @InProceedings{BlomEtal01, author = "Stefan Blom and Wan Fokkink and Jan Friso Groote and Izak van Langevelde and Bert Lisser and Jaco van de Pol", title = "{$\mu$CRL:} A Toolset for Analysing Algebraic Specifications", booktitle = "Proceedings of the 13th Conference on Computer-Aided Verification (CAV'01)", pages = "250--254", year = "2001", editor = "G\'erard Berry and Hubert Comon and Alain Finkel", volume = "2102", series = "Lecture Notes in Computer Science", month = jul, publisher = "Springer", } @Book{GeistAandB94a, author = "A Geist and A Beguelin and J Dongarra and W Jiang and R Manchek and V Sunderam", publisher = "MIT Pres", title = "{PVM}: Parallel Virtual Machine. {A} Users' Guide and Tutorial for Networked Parallel Computing", year = "94", url = "http://www.netlib.org/pvm3/book/pvm-book.html", keywords = "PVM, tutorial", series = "Scientific and Engineering Computation", scope = "pvmmpi", } @InProceedings{GrumbergHS01, author = "Orna Grumberg and Tamir Heyman and Assaf Schuster", title = "Distributed Symbolic Model Checking for $\mu$-Calculus", booktitle = "Proceedings of the 13th Conference on Computer-Aided Verification (CAV'01)", pages = "350--362", year = "2001", editor = "G\'erard Berry and Hubert Comon and Alain Finkel", volume = "2102", series = "Lecture Notes in Computer Science", month = jul, publisher = "Springer", } @Article{IC::VardiW1994, refkey = "C994", title = "Reasoning About Infinite Computations", author = "Moshe Y. Vardi and Pierre Wolper", pages = "1--37", journal = "Information and Computation", month = "15~" # nov, year = "1994", volume = "115", number = "1", abstract = "We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions (finite, looping and repeating) for the automata. It turns out, however, that these logics all have the same expressive power and that their decision problems are all PSPACE-complete. We also investigate connectives defined by alternating automata and show that they do not increase the expressive power of the logic or the complexity of the decision problem.", references = "LICS::AlurH1990, TLS::BanieqbalB1989, TLS::BanieqbalBP1989, FMP::BarringerKP1985, POPL::BarringerKP1986, TCS::BrzozowskiL1980, PICLMPS::Buchi1960, JACM::ChandraKS1981, JCSS::Choueka1974, ICALP::EmersonC1980:169, JCSS::FischerL1979, POPL::GabbayPSS1980, TCS::HalpernR1983, MISC::Harel1979, MISC::Harel1984, JCSS::HarelKP1982, POPL::HarelP1978, TCS::HarelP1985, LICS::HarelRV1990, IC::HarelS1982, IC::HarelS1985, JCSS::Jones1975, TCS::Kaminski1985:217, TCS::Kozen1983, IC::Ladner1977, IEEETSE::Lamport1977, MST::Landweber1969, TCS::Leiss1981:323, WLP::LichtensteinPZ1985, LNCS::MannaP1989, TOPLAS::MannaW1984, IC::McNaughton1966, LOGIC::Meyer1975, AMSSCC::MeyerS1973, BOOK::Milner1980, TCS::MiyanoH1984, TCS::MoriyaY1988, FOCS::Muller1963, LICS::MullerSS1988, ACTAI::Nishimura1980, FOCS::Pnueli1977, POPL::PnueliR1989, FOCS::Pratt1976, FOCS::Pratt1979, JCSS::Pratt1980, WLP::Pratt1982, IBMJRD::RabinS1959, FOCS::Safra1988, TR::Shaw1979, THESIS::Sistla1983, JACM::SistlaC1985, TCS::SistlaVW1987, EIVK::Staiger1987, IC::Streett1982, IC::Thomas1979, IC::Thomas1981, HTCS::Thomas1990, BOOK::TrakhtenbrotB1973, FOCS::Vardi1985, WLP::Vardi1985, POPL::Vardi1988, WLP::VardiW1983, JCSS::VardiW1986, LICS::VardiW1986, IC::Wagner1979, THESIS::Wolper1982, IC::Wolper1983, TLS::Wolper1989", references = "\cite{LICS::AlurH1990} \cite{TLS::BanieqbalB1989} \cite{TLS::BanieqbalBP1989} \cite{FMP::BarringerKP1985} \cite{POPL::BarringerKP1986} \cite{TCS::BrzozowskiL1980} \cite{PICLMPS::Buchi1960} \cite{JACM::ChandraKS1981} \cite{JCSS::Choueka1974} \cite{ICALP::EmersonC1980} \cite{JCSS::FischerL1979} \cite{POPL::GabbayPSS1980} \cite{TCS::HalpernR1983} \cite{MISC::Harel1979} \cite{MISC::Harel1984} \cite{JCSS::HarelKP1982} \cite{POPL::HarelP1978} \cite{TCS::HarelP1985} \cite{LICS::HarelRV1990} \cite{IC::HarelS1982} \cite{IC::HarelS1985} \cite{JCSS::Jones1975} \cite{TCS::Kaminski1985} \cite{TCS::Kozen1983} \cite{IC::Ladner1977} \cite{IEEETSE::Lamport1977} \cite{MST::Landweber1969} \cite{TCS::Leiss1981} \cite{WLP::LichtensteinPZ1985} \cite{LNCS::MannaP1989} \cite{TOPLAS::MannaW1984} \cite{IC::McNaughton1966} \cite{LOGIC::Meyer1975} \cite{AMSSCC::MeyerS1973} \cite{BOOK::Milner1980} \cite{TCS::MiyanoH1984} \cite{TCS::MoriyaY1988} \cite{FOCS::Muller1963} \cite{LICS::MullerSS1988} \cite{ACTAI::Nishimura1980} \cite{FOCS::Pnueli1977} \cite{POPL::PnueliR1989} \cite{FOCS::Pratt1976} \cite{FOCS::Pratt1979} \cite{JCSS::Pratt1980} \cite{WLP::Pratt1982} \cite{IBMJRD::RabinS1959} \cite{FOCS::Safra1988} \cite{TR::Shaw1979} \cite{THESIS::Sistla1983} \cite{JACM::SistlaC1985} \cite{TCS::SistlaVW1987} \cite{EIVK::Staiger1987} \cite{IC::Streett1982} \cite{IC::Thomas1979} \cite{IC::Thomas1981} \cite{HTCS::Thomas1990} \cite{BOOK::TrakhtenbrotB1973} \cite{FOCS::Vardi1985} \cite{WLP::Vardi1985} \cite{POPL::Vardi1988} \cite{WLP::VardiW1983} \cite{JCSS::VardiW1986} \cite{LICS::VardiW1986} \cite{IC::Wagner1979} \cite{THESIS::Wolper1982} \cite{IC::Wolper1983} \cite{TLS::Wolper1989}", url = "http://www.cs.rice.edu/~vardi/papers/focs83rj.ps.gz", } @InProceedings{EmersonLei85, author = "E. Allen Emerson and Chin-Laung Lei", title = "Modalities for Model Checking: Branching Time Strikes Back", booktitle = "Conference Record of the Twelfth Annual {ACM} Symposium on Principles of Programming Languages", address = "New Orleans, Louisiana", organization = "ACM SIGACT-SIGPLAN", publisher = "ACM Press", month = jan # " 13--16,", year = "1985", pages = "84--96", note = "Extended abstract", } @Book{CLR90, author = "T.~H. Cormen and C.~E. Leiserson and R.~L. Rivest", year = "1990", title = "Introduction to algorithms", edition = "6th", publisher = "MIT Press and McGraw-Hill Book Company", } @InCollection{Thomas99, author = "Wolfgang Thomas", title = "Complementation of {B}{\"u}chi Automata revisited", booktitle = "Jewels are forever -- Contributions on Theoretical Computer Science in Honor of {Arto Salomaa}", editor = "Juhani Karhum{\"a}ki and others", publisher = "Springer", pages = "109--122", year = "1999", } @Article{KupfermanV01, author= {Orna Kupferman and Moshe Y. Vardi}, title= {Weak Alternating Automata Are Not That Weak}, journal= {ACM Transactions on Computational Logic}, year= {2001}, volume= {2}, number= {3}, pages= {408--429}, } @Unpublished{Michel88, author= {Max Michel}, title= {Complementation is more difficult with automata on infinite words}, note = {CNET, Paris}, year= {1988}, } @InProceedings{ICALP::SistlaVW1985, title = "The Complementation Problem for {B{\"u}chi} Automata with Applications to Temporal Logic (Extended Abstract)", author = "A. Prasad Sistla and Moshe Y. Vardi and Pierre Wolper", editor = "Wilfried Brauer", booktitle = "Automata, Languages and Programming, 12th Colloquium", address = "Nafplion, Greece", month = "15--19~" # jul, year = "1985", series = "Lecture Notes in Computer Science", volume = "194", publisher = "Springer", pages = "465--474", } @InProceedings{Safra88, author = {Safra, Shmuel}, title = {On the Complexity of omega-Automata }, booktitle = {Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS'88}, pages = {319--327}, year = {1988}, month = {October}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, California} } @InProceedings{Klarlund91, author = {Nils Klarlund}, title = {Progress Measures for Complementation of omega-Automata with Applications to Temporal Logic}, booktitle = {Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, FoCS'91}, pages = {358--367}, publisher = {IEEE Computer Society Press}, year = 1991 } @Article{JCSS::Jones1975, title = "Space-Bounded Reducibility among Combinatorial Problems", author = "Neil D. Jones", pages = "68--85", journal = "Journal of Computer and System Sciences", year = "1975", month = aug, volume = "11", number = "1", } @InCollection{Dedekind1897, author = "R. Dedekind", title = "{\"Uber Zerlegungen von Zahlen durch ihre gr\"ossten gemeinsamen Teiler}", booktitle = "Richard Dedekind. Gesammelte mathematische Werke", editor = "Robert Fricke and Emmy Noether and {\"O}ystein Ore", volume = "II", pages = "103--148", note = "appeared 1897", year = "1969", publisher = "Chelsea Publishing Corporation", } @InProceedings{Kleitman69, author = {D. Kleitman}, title = {On {D}edekind's problem: the number of monotone {B}oolean functions}, booktitle = {5--th Proceedings of the American Mathematics Society}, pages = {677--682}, year = 1969, volume = 21 } @InProceedings{MullerSS86, author= {David E. Muller and Ahmed Saoudi and Paul E. Schupp}, title= {Alternating automata, the weak monadic theory of the tree, and its complexity}, booktitle= {Proceedings of the 13th International Colloquium on Automata, Languages and Programming, ICALP'86}, pages= {275--283}, year= 1986, volume= 226, series= {Lecture Notes in Computer Science}, publisher= {Springer}, } @Article{MiyanoH84, author= {Satoru Miyano and Takeshi Hayashi}, title= {Alternating finite automata on {$\omega$}-words}, journal= {Theoretical Computer Science}, year= {1984}, volume= {32}, pages= {321--330}, } @Article{MullerS87, author = {David E. Muller and Paul E. Schupp}, title = {Alternating automata on infinite trees}, journal = {Theoretical Computer Science}, year = 1987, volume = 54, pages = {267-276} } @InProceedings{KupfermanV97, author = {Orna Kupferman and Moshe Y. Vardi}, title = {Weak Alternating Automata Are Not That Weak }, booktitle = {Proceedings of the Fifth Israel Symposium on Theory of Computing and Systems, ISTCS'97}, pages = {147--158}, year = {1997}, publisher = {IEEE Computer Society Press}, address = {Los Alamitos, California} } @InProceedings{Vardi01a, author = "Moshe Y. Vardi", title = "Branching vs. Linear Time: Final Showdown", booktitle = "Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)", pages = "1--22", year = "2001", editor = "Tiziana Margaria and Wang Yi", volume = 2031, series = "Lecture Notes in Computer Science", month = apr, publisher = "Springer", } @Article{HalpernHIKVV01, author = {Joseph Y. Halpern and Robert Harper and Neil Immerman and Phokion G. Kolaitis and Moshe Y. Vardi and Victor Vianu}, title = {On the unusual effectiveness of logic in computer science}, journal = {The Bulletin of Symbolic Logic}, year = 2001, volume = 7, number = 2, pages = {213--236}, month = {jun} } @Book{Fokkink00a, author = "Wan Fokkink", title = "Introduction to Process Algebra", publisher = "Springer", year = "2000", ISBN = "3-540-66579-X", } @InProceedings{MilPMMCA, author = "R. Milner", title = "Processes, a Mathematical Model of Computing Agents", booktitle = "Logic Colloquium, {B}ristol 1973", pages = "157--174", publisher = "North-Holland", year = "1975", } @Article{Bergstra1984, author = "J. A. Bergstra and J. W. Klop", title = "Process Algebra for Synchronous Communication", journal = "Information and Control", volume = "60", year = "1984", pages = "109--137", references = "44", country = "USA", language = "English", enum = "4102", descriptors = "Process interaction; concurrency; process algebra;", date = "08/01/91", by_date = "LS", revision = "21/04/91", by_rev = "Le", location = "RWTH-AC-DFV: Bibl.", annote = "Within the context of an algebraic theory of processes, an equational specification of process cooperation is provided. The rewrite system behind the communication algebra is shown to be confluent and terminating. Further, some relationships are shown to hold between the concepts of merging.", } @Article{PeledWilWol98, author = "Doron Peled and Thomas Wilke and Pierre Wolper", title = "An Algorithmic Approach for Checking Closure Properties of $\omega$-Regular Languages", journal = "Theoretical Computer Science", volume = "195", number = "2", pages = "183--203", year = "1998", note = "A preliminary version appeared in \cite{PeledWilWol96}", } @InProceedings{PeledWilWol96, author = "Doron Peled and Thomas Wilke and Pierre Wolper", title = "An Algorithmic Approach for Checking Closure Properties of $\omega$-Regular Languages", booktitle = {Proceedings of the 7th International Conference on Concurrency Theory (CONCUR'96)}, pages = {596--610}, year = 1996, volume = 1119, series = {Lecture Notes in Computer Science}, address = {Pisa,Italy}, publisher = {Springer} } @Article{HennessyMilner85, author = "M. Hennessy and R. Milner", journal = "Journal of the ACM", pages = "137--162", title = "Algebraic laws for indeterminism and concurrency", volume = "32", year = "1985", } @Book{Stirling01, author = {Colin Stirling}, title = {Modal and Temporal Properties of Processes}, publisher = {Springer}, year = 2001, series = {Texts in Computer Science} } @Article{KatzPeled91, author = "Shmuel Katz and Doron Peled", title = "Interleaving Set Temporal Logic", journal = "Theoretical Computer Science", volume = "75", number = "3", year = "1991", pages = "21--43", note = "Preliminary versions appeared in 6th Annual ACM Symposium on Distributed Computing 1987, and in LNCS 398, Temporal Logic in Specification, 1988", } @Techreport{Kuske01, Author = "Dietrich Kuske", Title = "Another step towards a theory of regular {MSC} languages", Institution = "Department of Mathematics and Computer Science, University of Leicester", Year = "2001", Number = "36", } @InProceedings{Kuske02, author = "Dietrich Kuske", Title = "Another step towards a theory of regular {MSC} languages", booktitle = "Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02), 2002", publisher = "Springer", volume = "2285", series = "Lecture Notes in Computer Science", year = "2002", } @InProceedings{Morin02, author = "Remi Morin", Title = "Recognizable Sets of Message Sequence Charts", booktitle = "Proceedings of the 19th International Symposium on Theoretical Aspects of Computer Science (STACS'02), 2002", publisher = "Springer", volume = "2285", series = "Lecture Notes in Computer Science", year = "2002", } @InProceedings{GunterMuschollPeled01, author = "Elsa Gunter and Anca Muscholl and Doron Peled", title = "Compositional Message Sequence Charts", booktitle = "Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01)", pages = "496--511", year = "2001", editor = "Tiziana Margaria and Wang Yi", volume = 2031, series = "Lecture Notes in Computer Science", month = apr, publisher = "Springer", } @InProceedings{MadhusudanMeenakshi01, title = "Beyond Message Sequence Graphs", author = "P. Madhusudan and B. Meenakshi", booktitle = "Proceedings of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science", series = "Lecture Notes in Computer Science", volume = "2245", pages = "256--267", publisher = "Springer", year = "2001", pdf = Documents # "Madhusudan/beyondMSGs.pdf.gz", } @Book{Milner80, author = "R. Milner", title = "A Calculus for Communicating Processes", series = "Lecture Notes in Computer Science", volume = "92", publisher = "Springer", year = "1980", } @InProceedings{EmersonJS93, author = "E. A. Emerson and C. S. Jutla and A. P. Sistla", year = "1993", title = "On Model-Checking for Fragments of Mu-Calculus", booktitle = "Proc. 5th International Computer-Aided Verification Conference", pages = "385--396", editor = "C. Courcoubetis", series = "Lecture Notes in Computer Science", volume = "697", publisher = "Springer", } @InProceedings{BrimCKP01, title = "Distributed {LTL} Model-Checking Based on Negative Cycle Detection", booktitle = "Proceedings of 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'01)", author = "L. Brim and I. {\v{C}}ern{\'a} and P. Kr{\v{c}\'a}l and R. Pel{\'a}nek", editor = "", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "", month = dec, year = "2001", } @Book{Kropf99, author = {Thomas Kropf}, title = {Introduction to Formal Hardware Verification}, publisher = {Springer}, year = 1999 } @Book{Bruns97, author = {Glenn Bruns}, title = {Distributed Systems Analysis}, publisher = {Prentice Hall}, year = 1997 } @Book{TietzeSch01, author = "U. Tietze and Ch. Schenk", title = "Halbleiter-Schaltungstechnik", publisher = "Springer", year = "2001", edition = 11 } @Book{Chang99, author = {K. C. Chang}, title = {Digital Systems Design with "VHDL" and Synthesis}, publisher = {IEEE Computer Society Press}, year = 1999 } @Article{Mukund92, author = "M. Mukund", title = "Petri Nets and Step Transition Systems", journal = "IJFCS: International Journal of Foundations of Computer Science", volume = "3", year = "1992", } @Book{HandbookPA, title = "Handbook of Process Algebra", editor = "J. A. Bergstra and A. Ponse and S. A. Smolka", year = 2001, publisher = "Elsevier", } @Book{HandbookAR, title = {Handbook of Automated Reasoning}, editor = {A. Robinson and A. Voronkov}, year = 2001, publisher = "Elsevier", } @Incollection{Davis:HandbookAR:history:2001, title = {The Early History of Automated Deduction}, author = {M. Davis}, chapter = 1, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {3-15}} @Incollection{BachmairGanzinger:HandbookAR:resolution:2001, title = {Resolution Theorem Proving}, author = {L. Bachmair and H. Ganzinger}, chapter = 2, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {19-99}} @Incollection{Haehnle:HandbookAR:tableaux:2001, title = {Tableaux and Related Methods}, author = {R. H\"ahnle}, chapter = 3, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {100-178}} @Incollection{DegtyarevVoronkov:HandbookAR:inverse:2001, title = {The Inverse Method}, author = {A. Degtyarev and A. Voronkov}, chapter = 4, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {179-272}} @Incollection{Baaz+:HandbookAR:normal:2001, title = {Normal Form Transformations}, author = {M. Baaz and U. Egly and A. Leitsch}, chapter = 5, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {273-333}} @Incollection{NonnengartWeidenbach:HandbookAR:small:2001, title = {Computing Small Clause Normal Forms}, author = {A. Nonnengart and C. Weidenbach}, chapter = 6, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {335-367}} @Incollection{NieuwenhuisRubio:HandbookAR:paramodulation:2001, title = {Paramodulation-Based Theorem Proving}, author = {R. Nieuwenhuis and A. Rubio}, chapter = 7, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {371-443}} @Incollection{BaaderSnyder:HandbookAR:unification:2001, title = {Unification Theory}, author = {F. Baader and W. Snyder}, chapter = 8, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {445-532}} @Incollection{DershowitzPlaisted:HandbookAR:rewriting:2001, title = {Rewriting}, author = {N. Dershowitz and D.A. Plaisted}, chapter = 9, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {535-610}} @Incollection{DegtyarevVoronkov:HandbookAR:sequent:2001, title = {Equality Reasoning in Sequent-Based Calculi}, author = {A. Degtyarev and A. Voronkov}, chapter = 10, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {611-706}} @Incollection{ChouGao:HandbookAR:geometry:2001, title = {Automated Reasoning in Geometry}, author = {S. C. Chou and X. S. Gao}, chapter = 11, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {707-749}} @Incollection{BockmayrWeispfenning:HandbookAR:numerical:2001, title = {Solving Numerical Constraints}, author = {A. Bockmayr and V. Weispfenning}, chapter = 12, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {751-842}} @Incollection{Bundy:HandbookAR:induction:2001, title = {The Automation of Proof by Mathematical Induction}, author = {A. Bundy}, chapter = 13, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {845-911}} @Incollection{Comon:HandbookAR:comon:2001, title = {Inductionless Induction}, author = {H. Comon}, chapter = 14, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {I}, pages = {913-962}} @Incollection{Andrews:HandbookAR:type:2001, title = {Classical Type Theory}, author = {P.B. Andrews}, chapter = 15, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {965-1007}} @Incollection{Dowek:HandbookAR:higher:2001, title = {Higher-Order Unification and Matching}, author = {G. Dowek}, chapter = 16, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1009-1062}} @Incollection{Pfenning:HandbookAR:framework:2001, title = {Logical Frameworks}, author = {F. Pfenning}, chapter = 17, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1063-1147}} @Incollection{BarendregtGeuvers:HandbookAR:assistant:2001, title = {Proof-Assistants Using Dependent Type Systems}, author = {H. Barendregt and H. Geuvers}, chapter = 18, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1149-1238}} @Incollection{Dix+:HandbookAR:nmr:2001, title = {Nonmonotonic Reasoning: Towards Efficient Calculi and Implementations}, author = {J. Dix and U. Furbach and I. Niemel{\"a}}, chapter = 19, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1241-1354}} @Incollection{Baaz+:HandbookAR:manyvalued:2001, title = {Automated Deduction for Many-Valued Logics}, author = {M. Baaz and C.G. Ferm{\"u}ller and G. Salzer}, chapter = 20, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1355-1402}} @Incollection{Ohlbach+:HandbookAR:encoding:2001, title = {Encoding Two-Valued Nonclassical Logics in Classical Logic}, author = {H.J. Ohlbach and A. Nonnengart and M.\ de Rijke and D.\ Gabbay}, chapter = 21, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1403-1486}} @Incollection{Waaler:HandbookAR:nonclassical:2001, title = {Connections in Nonclassical Logics}, author = {A. Waaler}, chapter = 22, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1487-1578}} @Incollection{Calvanese+:HandbookAR:dl:2001, title = {Reasoning in Expressive Description Logics}, author = {D. Calvanese and G. De Giacomo and M. Lenzerini and D. Nardi}, chapter = 23, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1581-1634}} @Incollection{ClarkeSchlingloff:HandbookAR:checking:2001, title = {Model Checking}, author = {E.M. Clarke and H. Schlingloff}, chapter = 24, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1635-1790}} @Incollection{Fermuller+:HandbookAR:decision:2001, title = {Resolution Decision Procedures}, author = {C.~Ferm{\"u}ller and A. Leitsch and U. Hustadt and T. Tammet}, chapter = 25, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1791-1849}} @Incollection{Ramakrishnan+:HandbookAR:term:2001, title = {Term Indexing}, author = {I.V. Ramakrishnan and R. Sekar and A. Voronkov}, chapter = 26, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1853-1964}} @Incollection{Weidenbach:HandbookAR:spass:2001, title = {Combining Superposition, Sorts and Splitting}, author = {C. Weidenbach}, chapter = 27, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {1965-2013}} @Incollection{LetzStenz:HandbookAR:me:2001, title = {Model Elimination and Connection Tableau Procedures}, author = {R. Letz and G. Stenz}, chapter = 28, booktitle = {Handbook of Automated Reasoning}, publisher = {Elsevier Science}, editor = {A. Robinson and A. Voronkov}, year = 2001, volume = {II}, pages = {2015-2114}} @TechReport{MKS95, author = "M. Mukund and K. Narayan Kumar and M. Sohoni", title = "Keeping track of the latest gossip in message-passing systems", institution = "School of Mathematics, SPIC Science Foundation", year = "1995", number = "TCS-95-3", address = "Madras, India", } @InProceedings{STOC::SistlaC1982, title = "The Complexity of Propositional Linear Temporal Logics", author = "A. P. Sistla and E. M. Clarke", pages = "159--168", booktitle = "Proceedings of the Fourteenth Annual {ACM} Symposium on Theory of Computing", month = "5--7 " # may, year = "1982", address = "San Francisco, California", } @Article{SistlaC85, author = "A. P. Sistla and E. M. Clarke", title = "Complexity of Propositional Temporal Logics", journal = {Journal of the ACM}, year = 1985, volume = 32, pages = {733--749} } @InCollection{Leucker01, author = {Martin Leucker}, title = {Prefix-Recognizable Graphs and Monadic Second Order Logic}, booktitle = {Automata, Logics and Infinite Games}, publisher = {Springer}, year = 2002, editor = {Erich Gr{\"a}del and Wolfgang Thomas and {Th}omas Wilke}, volume = "2500", pages = "263--283", series = "Lecture Notes in Computer Science", url = "http://link.springer.de/link/service/series/0558/papers/2500/25000263.pdf", pdf = Documents # "Leucker/PrgMSO.pdf.gz" } @Article{ClarkeW96, author = "Edmund M. Clarke and Jeanette M. Wing", title = "Formal Methods: {S}tate of the Art and Future Directions", journal = "ACM Computing Surveys", year = "1996", volume = "28", number = "4", pages = "626--643", month = dec, } @Book{UsingUML, author = {Perdita Stevens and Rob Pooley}, title = {Using {UML}: software engineering with objects and components}, publisher = {Addison-Wesley Longman}, year = 1999, series = "Object Technology Series", isbn = "0201648601", note = {Updated edition for UML1.3: first published 1998 (as Pooley and Stevens)} } @Book{Katoen99, author = {Joost-Pieter Katoen}, title = {Concepts, Algorithms and Tools for Model Checking}, publisher = {Friedrich-Alexander-Universit{\"a}t Erlangen N{\"u}rnberg}, year = 1999, volume = {32-1}, series = {Arbeitsberichte der Informatik} } @InProceedings{ayari.ea:lisa:1997, author = "Abdelwaheb Ayari and David Basin and Andreas Podelski", title = "{LISA}: {A} Specification Language Based on {WS2S}", booktitle = "11th International Conference of the European Association for Computer Science Logic (CSL'97)", year = "1997", series = "Lecture Notes in Computer Science", volume = "1414", pages = "18--34", publisher = "Springer", editor = "Mogens Nielsen and Wolfgang Thomas", language = "USenglish", ps = "http://wailoa.informatik.uni-freiburg.de/WebBIB/publications/papers/1997/lisa.ps.gz", abstract = "We integrate two concepts from programming languages into a specification language based on WS2S, namely high-level data structures such as records and recursively-defined datatypes (WS2S is the weak second-order monadic logic of two successors). Our integration is based on a new logic whose variables range over record-like trees and an algorithm for translating datatypes into tree automata. We have implemented Lisa, a prototype system based on these ideas, which, when coupled with a decision procedure for WS2S like the Mona system, results in a verification tool that supports both high-level specifications and complexity estimations for the running time of the decision procedure.", } @InProceedings{Henriksen:1995:MMS, author = "Jesper G. Henriksen and Jakob L. Jensen and Michael E. J{\o}rgensen and Nils Klarlund and Robert Paige and Theis Rauhe and Anders Sandholm", title = "{M}ona: Monadic Second-Order Logic in Practice", editor = "Ed Brinksma and Rance Cleaveland and Kim Guldstrand Larsen and Tiziana Margaria and Bernhard Steffen", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", publisher = "Springer", volume = "1019", year = "1995", ISBN = "3-540-60630-0", pages = "89--110", annote = "incomplete", } @InProceedings{ClarkeE81, address = "Yorktown Heights, New York", author = "E. M. Clarke and E. A. Emerson", booktitle = "Proceedings of the Workshop on Logics of Programs", editor = "D. Kozen", month = may, pages = "52--71", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "{D}esign and {S}ynthesis of {S}ynchronization {S}keletons using {B}ranching {T}ime {T}emporal {L}ogic", volume = "131", year = "1981", } @Book{GammaEtAl00, author = "Gamma and Helm and Johnson and Vlissides", title = "Design Patterns Elements of Reusable Object-Oriented Software", publisher = "Addison-Wesley", address = "Massachusetts", year = "2000", ISBN = "0-201-63361-2", } @Book{BowenHinchey99b, title = "Industrial-Strength Formal Methods in Practice", editor = "Jonathan P. Bowen and Michael G. Hinchey", publisher = "Springer", series = "Formal Approaches to Computing and Information Technology", year = "1999", isbn_issn = "1-85233-640-4", } @Book{CartierF69, author = "Pierre Cartier and Dominique Foata", address = "Berlin-Heidelberg-New York", number = "85", publisher = "Springer", series = "Lecture Notes in Mathematics", title = "Probl\`emes combinatoires de commutation et r{\'e}ar\-ran\-ge\-ments", year = "1969", annote = "The lecture notes introduces the theory of free partially commutative monoids. It defines its M{\"o}bius function and the Foata normal form is presented. Various combinatorical identities are shown. Among others a generalization of the Master Theorem of MacMahon is given. A source of deep and rich combinatorial results.", } @InProceedings{DiekertGastin01, author = {Volker Diekert and Paul Gastin}, title = {Local Temporal Logic is Expressively Complete for Cograph Dependence Alphabets}, booktitle = {Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'01)}, pages = {55-69}, year = 2001, editor = {R. Nieuwenhuis and A. Voronkov}, volume = 2250, series = {Lecture Notes in Artificial Intelligence}, publisher = {Springer} } @Article{IC::Thomas1979, title = "Star-Free Regular Sets of $\omega$-Sequences", author = "Wolfgang Thomas", pages = "148--156", journal = "Information and Control", month = aug, year = "1979", volume = "42", number = "2", } @InProceedings{Thomas90, author = {Wolfgang Thomas}, title = {On logical definability of trace languages}, booktitle = {Proceedings of a workshop of the {ESPRIT} Basic Research Action No 3166: Algebraic and Syntactic Methods in Computer Science (ASMICS)}, pages = {172-182}, year = 1990, editor = {Volker Diekert}, series = {TUM-I9002}, address = {Kochel am See, Bavaria}, publisher = {Technical University of Munich} } @InProceedings{QuSi82, address = "New York", author = "J.P. Queille and J. Sifakis", booktitle = "Proceedings of the Fifth International Symposium in Programming", key = "QuSi82", pages = "337--351", publisher = "Springer", series = "Lecture Notes in Computer Science", title = "Specification and Verification of Concurrent Systems in {CESAR}", volume = "137", year = "1982", } @PhdThesis{Leucker02, author = {Martin Leucker}, title = {Logics for Mazurkiewicz traces}, school = {Lehrstuhl f\"ur Informatik II, RWTH Aachen}, year = 2002, url = "http://aib.informatik.rwth-aachen.de/2002/2002-10.pdf", postscript = "http://aib.informatik.rwth-aachen.de/2002/2002-10.ps.gz", pdf = Documents # "Leucker/2002-10.pdf.gz", } @InProceedings{HiarishiHOY91, author = "H. Hiraishi and K. Hamaguchi and H. Ochi and S. Yajima", title = "Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification", pages = "214--224", ISBN = "3-540-55179-4", editor = "Kim G. Larsen and Arne Skou", booktitle = "Proceedings of Computer Aided Verification ({CAV} '91)", month = jul, series = "LNCS", volume = "575", publisher = "Springer", address = "Berlin, Germany", year = "1992", } @InProceedings{BLN02, author = "Benedikt Bollig and Martin Leucker and Thomas Noll", title = "Generalised Regular {MSC} Languages", booktitle = "Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS '02)", pages = "52--66", year = "2002", editor = "Mogens Nielsen", volume = "2303", series = "Lecture Notes in Computer Science", month = "", publisher = "Springer-Verlag Inc.", } @InProceedings{BLW02, author = "Benedikt Bollig and Martin Leucker and Michael Weber", title = "Local Parallel Model Checking for the Alternation-Free mu-Calculus", booktitle = "Proceedings of the 9th International SPIN Workshop on Model checking of Software (SPIN '02)", pages = "", year = "2002", editor = "", volume = "2318", series = "Lecture Notes in Computer Science", month = "", publisher = "Springer-Verlag Inc.", seealso = "BolligLeuckerWeber01", pdf = Documents # "Leucker/spin2002.pdf.gz", } @Article{Garavel:1998:OCO, author = "Hubert Garavel", title = "{OPEN\slash CAESAR}: An Open Software Architecture for Verification, Simulation, and Testing", journal = "Lecture Notes in Computer Science", volume = "1384", pages = "68--??", year = "1998", coden = "LNCSD9", ISSN = "0302-9743", bibdate = "Tue Feb 5 11:51:51 MST 2002", url = "http://link.springer-ny.com/link/service/series/0558/bibs/1384/13840068.htm; http://link.springer-ny.com/link/service/series/0558/papers/1384/13840068.pdf", acknowledgement = ack-nhfb, } @Book{Diestel00, author = "Reinhard Diestel", title = "Graph theory", publisher = "Springer-Verlag", edition = "2", year = "2000", address = "New York", pages = "312", url = "http://www.math.uni-hamburg.de/home/diestel/books/graph.theory/GraphTheoryII.pdf", } @InProceedings{Madhusudan01, author = "P. Madhusudan", title = "Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs", editor = "F. Orejas and P. G. Spirakis and J. van Leeuwen", booktitle = "Proceedings of 27th International Colloquium on Automata, Languages and Programming (ICALP'2000)", year = "2001", series = "Lecture Notes in Computer Science", volume = "2076", pages = "396--407", publisher = "Springer-Verlag Inc.", } @InProceedings{Peled00, author = {Doron Peled}, title = {Specification and verification of message sequence charts}, booktitle = {Proc. IFIP FORTE/PSTV}, year = 2000, pages = {139--154}, } @Article{BolligLeucker02a, author = {Benedikt Bollig and Martin Leucker}, title = {Deciding {LTL} over {M}azurkiewicz Traces}, journal = {Data \& Knowledge Engineering}, year = 2003, volume = {44/2}, pages = {221--240}, month = feb, url = "http://www.sciencedirect.com/science?_ob=GatewayURL&_origin=compsciportal&_method=citationSearch&_urlversion=4&_version=1&_piikey=S0169023X02001362&md5=f40b45623c37bf5cda16337b84ccffe5", } @TechReport{BolligLeuckerLucas02, author = "Benedikt Bollig and Martin Leucker and Philipp Lucas", title = "Extending Compositional Message Sequence Graphs", institution = "University of Pennsylvania", year = "2002", number = "MS-CIS-02-09", month = apr, url = "http://www.cis.upenn.edu/~techreports/abstracts02.html", pdf = Documents # "Leucker/MS-CIS-02-09.pdf.gz", } @InProceedings{Kesten97a, author = "Y. Kesten and O. Maler and M. Marcus and A. Pnueli and E. Shahar", year = "1997", title = "Symbolic Model Checking with Rich Assertional Languages", booktitle = "Proceedings of 9th International Conference on Computer-Aided Verification (CAV'97)", pages = "424--435", abstract = "The paper shows that, by an appropriate choice of a rich assertional language, it is possible to extend the utility of symbolic model checking beyond the realm of BDD-represented finite-state systems into the domain of infinite-state systems, leading to a powerful technique for uniform verification of unbounded (parameterized) process networks. The main contributions of the paper are a fomulation of a general framework for symbolic model checking of infinite-state systems, a demonstration that many individual examples of uniformly verified parameterized designs that appear in the literature are special cases of our general approach, verifying the correctness of the Futurebus+ design for all singlebus configurations, extending the technique to tree architectures, and establishing that the presented method is a precise dual to the top-down invariant generation method used in deductive verification.", series = "Lecture Notes in Computer Science", VOLUME = "1254", } @Article{Kesten:2001:SMC, author = "Y. Kesten and O. Maler and M. Marcus and A. Pnueli and E. Shahar", title = "Symbolic model checking with rich assertional languages", journal = "Theoretical Computer Science", volume = "256", number = "1--2", pages = "93--112", day = "6", month = apr, year = "2001", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Tue Apr 17 08:40:31 MDT 2001", url = "http://www.elsevier.nl../26/abstract.html; http://www.elsevier.nl/gej%2Dng/10/41/16/198/21/26/article.pdf", } @InProceedings{BJNT00, author = "Ahmed Bouajjani and Bengt Jonsson and Marcus Nilsson and Tayssir Touili", title = "Regular Model Checking", booktitle = "Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00)", editor = "E. A. Emerson and A. P. Sistla", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1855", year = "2000", pages = "403--418", } @InProceedings{AJ00, author = "Parosh Azis Abdulla and Bengt Jonsson", title = "Verification of Infinite-State and Parameterized Systems", booktitle = "Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00)", editor = "E. A. Emerson and A. P. Sistla", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1855", year = "2000", } @InProceedings{PS00, author = "Amir Pnueli and Elad Shahar", title = "Liveness and Acceleration in Parameterized Verification", booktitle = "Proceedings of the 12th International Conference on Computer-Aided Verification (CAV'00)", editor = "E. A. Emerson and A. P. Sistla", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "1855", year = "2000", postscript = Documents # "Pnueli/cav00.ps.gz", } @InProceedings{EmersonV02, author = "E. Allen Emerson and Vineet Kahlon", title = "Model Checking Large-Scale and Parameterized Resource Allocation Systems", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)", editor = "J.-P. Katoen, P. Stevens", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "2280", year = "2002", pages = "251--265", } @InProceedings{Cou97, author = "B. Courcelle", title = "On the expression of graph properties in some fragments of monadic second-order logic", booktitle = "Descriptive complexity and finite models", volume = "31", month = "June", publisher = "DIMACS Series in Discrete Mathematics and Theoretical Computer Sciences", editor = "N. Immerman and P.Kolaitis", pages = "33--62", year = "1997"} @InProceedings{HongLSU02, author = {Hyoung Seok Hong and Insup Lee and Oleg Sokolsky and Hasan Ural}, title = {A Temporal Logic Based Theory of Test Coverage and Generation}, booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)", editor = "J.-P. Katoen, P. Stevens", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = 2280, pages = {327--241}, year = 2002, url = "http://link.springer.de/link/service/series/0558/papers/2280/22800327.pdf", } @InProceedings{SchmidtSt98, author = "D. Schmidt and B. Steffen", title = "Program Analysis as Model Checking of Abstract Interpretations", booktitle = "Proc. 5th Static Analysis Symposium", series = "Lecture Notes in Computer Science", publisher = "Springer", editor = "G. Levi", volume = "1503", pages = "351--381", year = "1998", url = "http://www.cis.ksu.edu/~schmidt/papers/paperneu9.ps.Z", } @InProceedings{MauwR97, author = "S. Mauw and M. A. Reniers", title = "High-level message sequence charts", booktitle = "Proceedings of the Eighth {SDL} Forum {(SDL'97)}", year = "1997", pages = "291--306", abstract = "We study High-level Message Sequence Charts -- a concept incorporated into MSC96 for composing MSCs explicitly. A formal semantics is given which extends the accepted process algebra semantics of MSC92. We assess the language by studying a simple example, which leads us to consider the extension of HMSC with gates.", } @Article{CY1995, title = "The Complexity of Probabilistic Verification", author = "Costas Courcoubetis and Mihalis Yannakakis", pages = "857--907", area = "Logic in Computer Science", journal = "Journal of the ACM", month = jul, year = "1995", volume = "42", number = "4", general-terms = "Algorithms, Theory, Verification", keywords = "Automata, EXPTIME-complete, Markov chain, model checking, probabilistic algorithm, PSPACE-complete, temporal logic", cr-categories = "D.2.4; F.2.2 [complexity of proof procedures]; F.3.1 [mechanical verification]; G.3 [probabilistic algorithms]", references = "\cite{JACM::ChandraKS1981} \cite{POPL::ClarkeES1983} \cite{POPL::EmersonH1983} \cite{POPL::EmersonL1985} \cite{FOCS::FrancezR1980} \cite{POPL::GabbayPSS1980} \cite{STOC::HartS1984} \cite{TOPLAS::HartSP1983} \cite{POPL::LehmannR1981} \cite{IC::LehmannS1982} \cite{POPL::LichtensteinP1985} \cite{IC::McNaughton1966} \cite{LICS::PnueliZ1986} \cite{STOC::Pnueli1983} \cite{FOCS::Safra1988} \cite{JACM::SistlaC1985} \cite{FOCS::Vardi1985} \cite{LICS::VardiW1986} \cite{FOCS::WolperVS1983} \cite{IC::Wolper1983}", } @Article{PZ1993, title = "Probabilistic Verification", author = "Amir Pnueli and Lenore D. Zuck", pages = "1--29", journal = "Information and Computation", month = mar, year = "1993", volume = "103", number = "1", xxx-references = "FOCS::CourcoubetisY88, Feldman84, LehmannS82, FOCS::Pnueli77, JACM::SistlaC85, FOCS::Vardi85, LICS::VardiW86, FOCS::Wolper81", references = "\cite{FOCS::CourcoubetisY1988} \cite{IC::Feldman1984} \cite{IC::LehmannS1982} \cite{FOCS::Pnueli1977} \cite{JACM::SistlaC1985} \cite{FOCS::Vardi1985} \cite{LICS::VardiW1986} \cite{FOCS::Wolper1981}", } @InProceedings{Vardi1985, title = "Automatic Verification of Probabilistic Concurrent Finite-State Programs", author = "Moshe Y. Vardi", pages = "327--338", booktitle = "26th Annual Symposium on Foundations of Computer Science", month = "21--23 " # oct, year = "1985", address = "Portland, Oregon", organization = "IEEE", } @Book{KS1960, author = "J. G. Kemeny and J. L. Snell", title = "Finite Markov Chains", publisher = "Van Nostrand Reinhold", address = "New York", year = "1960", ISBN = "0-442-04328-7", descriptor = "Markovkette, Stochastischer Prozess, Wahrscheinlichkeitsrechnung", annote = "1. Prerequesites 2. Basic concepts of Markov chains 3. Absorbing Markov chains 4. Regular Markov chains 5. Ergodic Markov chains 6. Further results 7. Applications of Markov chains Appendices", } @Techreport{DammH98, author = {Werner Damm and David Harel}, title = {{LSC's}: Breathing Life into Message Sequence Charts}, number = {CS98-09}, institution = {Weizmann Institute of Science}, month = apr, year = 1998 } @InProceedings{LNSW01, author = {Martin Leucker and Thomas Noll and Perdita Stevens and Michael Weber}, title = {Functional programming languages for verification tools: experiences with {ML} and {H}askell }, booktitle = {Proceedings of the 3rd Scottish Functional Programming Workshop}, year = 2001, address = {University of Stirling}, postscript = Documents # "Leucker/sfpw.ps.gz", } @InProceedings{LeuckerNoll01b, author = {Martin Leucker and Thomas Noll}, title = {A Distributed Model Checking Tool Tailored to {E}rlang}, booktitle = {Proceedings of the Erlang Workshop}, year = 2001, } @InProceedings{BolligLeuckerLucas02b, author = {Benedikt Bollig and Martin Leucker and Philipp Lucas}, title = {Extending Compositional Message Sequence Graphs}, booktitle = {Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning ({LPAR'02})}, PUBLISHER = "Springer", series = "Lecture Notes in Artificial Intelligence", pages = {68--85}, year = 2002, editor = {Matthias Baaz and Andrei Voronkov}, volume = 2514, postscript = Documents # "Leucker/lpar02.ps.gz", pdf = Documents # "Leucker/lpar02.pdf.gz", } @InProceedings{DeussenT02, author = {Peter Deussen and Stephan Tobies}, title = {Formal test purposes and the validity of test cases}, booktitle = {22nd International Conference on Formal Techniques for Networked and Distributed Systems}, OPTcrossref = {}, OPTkey = {}, OPTpages = {}, year = 2002, OPTeditor = {}, OPTvolume = {}, OPTnumber = {}, OPTseries = {}, OPTaddress = {}, OPTmonth = {}, OPTorganization = {}, OPTpublisher = {}, OPTnote = {}, OPTannote = {}, postscript = Documents # "Deussen/forte02.ps.gz", } @InProceedings{1997:tacas:ben-abdallah, author = "Han{\^e}ne Ben-Abdallah and Stefan Leue", title = "Syntactic Detection of Process Divergence and Non-local Choice in Message Sequence Charts", editor = "Ed Brinksma", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems", series = "Lecture Notes in Computer Science", publisher = "Springer-Verlag", volume = "1217", year = "1997", ISBN = "3-540-62790-1", pages = "259--274", postscript = Documents # "BenAbdallah/tacas97.ps.gz" } @Article{Courcoubetis:1995:CPV, author = "Costas Courcoubetis and Mihalis Yannakakis", title = "The Complexity of Probabilistic Verification", journal = "Journal of the ACM", volume = "42", number = "4", pages = "857--907", month = jul, year = "1995", coden = "JACOAH", ISSN = "0004-5411", bibdate = "Tue Nov 28 07:53:44 1995", url = "http://www.acm.org/pubs/toc/Abstracts/0004-5411/210339.html", abstract = "We determine the complexity of testing whether a finite state, sequential or concurrent probabilistic program satisfies its specification expressed in linear-time temporal logic. For sequential programs, we present an algorithm that runs in time linear in the program and exponential in the specification, and also show that the problem is in PSPACE, matching the known lower bound. For concurrent programs, we show that the problem can be solved in time polynomial in the program and doubly exponential in the specification, and prove that it is complete for double exponential time. We also address these questions for specifications described by $\omega$-automata or formulas in extended temporal logic.", acknowledgement = ack-nhfb, keywords = "algorithms; theory; verification", subject = "{\bf F.3.1}: Theory of Computation, LOGICS AND MEANINGS OF PROGRAMS, Specifying and Verifying and Reasoning about Programs, Mechanical verification. {\bf D.2.4}: Software, SOFTWARE ENGINEERING, Program Verification. {\bf F.2.2}: Theory of Computation, ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY, Nonnumerical Algorithms and Problems, Complexity of proof procedures. {\bf G.3}: Mathematics of Computing, PROBABILITY AND STATISTICS, Probabilistic algorithms (including Monte Carlo). {\bf F.1.3}: Theory of Computation, COMPUTATION BY ABSTRACT DEVICES, Complexity Classes.", postscript = Documents # "Courcoubetis/complexity_probabilistic_mc.ps.gz", pdf = Documents # "Courcoubetis/complexity_probabilistic_mc.pdf.gz", } @PhdThesis{Mayr98, author = {Richard Mayr}, title = {Decidability and Complexity of Model Checking Problems for Infinite-State Systems}, school = {Technische Universit\"at M\"unchen}, year = 1998, month = apr, url = "http://www.informatik.uni-freiburg.de/~mayrri/diss_richard.ps", postscript = Documents # "Mayr/Dissertation.ps.gz", } @InProceedings{FOCS85*327, author = "M. Y. Vardi", title = "Automatic Verification of Probabilistic Concurrent Finite-State Programs", pages = "327--338", booktitle = "26th Annual Symposium on Foundations of Computer Science (FOCS'85)", ISBN = "0-8186-0644-4", month = oct, publisher = "IEEE Computer Society Press", address = "Los Angeles, Ca., USA", year = "1985", postscript = Documents # "Vardi/focs85.pdf.gz", } @PhdThesis{Shahar01, author = {Elad Shahar}, title = {Tools and Techniques for Verifying Paramerized Systems}, school = {Weizmann Institute of Science}, year = 2001, postscript = Documents # "Shahar/phdthesis.ps.gz", url = "http://www.wisdom.weizmann.ac.il/~elad/phdthesis.ps.Z", } @InProceedings{GenestM02, author = "Blaise Genest and Anca Muscholl", title = "Pattern Matching and Membership for Hierarchical Message Sequence Charts", booktitle = "Proceedings of the 5th Latin American Symposium on Theoretical Informatics (LATIN'02)", year = "2002", editor = "S. Rajsbaum", series = "Lecture Notes in Computer Science", volume = 2286, pages = "326--340", } @InProceedings{PelVY99a, author = "D. Peled and M. Vardi and M. Yannakakis", title = "Black Box Checking", booktitle = "Proc. FORTE/PSTV", publisher = "Kluwer", pages = "225--240", year = "1999", postscript = Documents # "pstv99.ps.gz", url = "http://www.cs.rice.edu/~vardi/papers/pstv99.ps.gz", } @Unpublished{Pel99b, author = "D. Peled and M. Vardi and M. Yannakakis", title = "Black Box Checking", booktitle = "Proc. FORTE/PSTV", publisher = "Kluwer", pages = "225--240", year = "1999", note = "extended version", postscript = Documents # "bbfull3.ps.gz", } @InProceedings{GrocePY02, author = "Alex Groce and Doron Peled and Mihalis Yannakakis", title = "Adaptive Model Checking", booktitle = "Tools and Algorithms for the Construction and Analysis of Systems (TACAS'02)", series = "Lecture Notes in Computer Science", volume = "2280", pages = "357--??", year = "2002", ISSN = "0302-9743", url = "http://link.springer-ny.com/link/service/series/0558/bibs/2280/22800357.htm", pdf = "http://link.springer-ny.com/link/service/series/0558/papers/2280/22800357.pdf", pdf = Documents # "Groce/tacas02.pdf.gz", } @InProceedings{LeuckerMM02, title = "Dynamic Message Sequence Charts", booktitle = "Proceedings of 22nd Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'02)", author = "Martin Leucker and P. Madhusudan and Supratik Mukhopadhyay", editor = "M. Agrawal and A. Seth", publisher = "Springer", series = "Lecture Notes in Computer Science", volume = "2556", month = dec, year = "2002", pdf = Documents # "Leucker/fsttcs02.pdf.gz", postscript = Documents # "Leucker/fsttcs02.ps.gz", } @TECHREPORT{Ramangalahy98, AUTHOR = {Ramangalahy, Solofo}, TITLE = {Strategies for Conformance Testing}, TYPE = {Research Report}, INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik}, ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany}, NUMBER = {MPI-I-98-2-010}, MONTH = {May}, YEAR = {1998}, ISSN = {0946-011X}, url = "http://data.mpi-sb.mpg.de/internet/reports.nsf/NumberView/1998-2-010", } @InProceedings{ClGL92, address = "New York", author = "E. Clarke and O. Grumberg and D. Long", booktitle = "Proceedings of the 19th Annual {ACM} Symposium on Principles of Programming Languages", keyword = "hardware verification modelchecking abstraction logic", pages = "342--354", month = jan, organization = "ACM", title = "{M}odel {C}hecking and {A}bstraction", year = "1992", } @InProceedings{WoLo89, address = "Grenoble, France", author = "P. Wolper and V. Lovinfosse", booktitle = "Proceedings of the International Workshop on Automatic Verification Methods for Finite State Systems", key = "WoLo89", pages = "68--80", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", title = "Verifying Properties of Large Sets of Processes with Network Invariants", volume = "407", year = "1989", } @Article{IC::KurshanM1995, refkey = "C1289", title = "A Structural Induction Theorem for Processes", author = "R. P. Kurshan and K. L. McMillan", pages = "1--11", journal = "Information and Computation", month = "15~" # feb, year = "1995", volume = "117", number = "1", abstract = "This paper deals with the formal verification of finite state systems that have an arbitrary number of isomorphic components. We present a technique for inductively generalizing tests on a system of fixed size in order to show that a system of arbitrary size satisfies a given specification. This makes it possible to use finite state verification systems, such as COSPAN, to verify parameterized protocols. The method also may be useful for verifying systems of fixed but large size, since it reduces the size of the system that must be checked automatically. The basis of the method is a {\em structural induction theorem\/} for processes, which is stated and proved in this paper. The theorem applies to a variety of process formalisms satisfying simple algebraic laws. We give examples of proofs using the Calculus of Communicating Systems (CCS) and the $s/r$ model.", xxx-references = "JACM::GermanS92, LICS::Walker88", references = "\cite{JACM::GermanS1992} \cite{LICS::Walker1988}", } @Article{Abadi:1991:ERM, author = "M. Abadi and L. Lamport", title = "The existence of refinement mappings", journal = "Theoretical Computer Science", volume = "82", number = "2", pages = "253--284", day = "31", month = may, year = "1991", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Sat Nov 22 13:24:22 MST 1997", acknowledgement = ack-nhfb, classification = "C4220 (Automata theory); C4240 (Programming and algorithm theory)", corpsource = "Digital Equipment Corp., Palo Alto, CA, USA", keywords = "automata theory; liveness requirements; lower-level specification; programming theory; refinement mappings; state machine", pubcountry = "Netherlands", } @Article{Abdulla:2002:MCS, author = "Parosh Aziz Abdulla and Bengt Jonsson", title = "Model checking of systems with many identical timed processes", journal = "Theoretical Computer Science", volume = "290", number = "1", pages = "241--264", month = oct, year = "2002", coden = "TCSCDI", ISSN = "0304-3975", bibdate = "Wed Nov 20 18:15:29 MST 2002", acknowledgement = ack-nhfb, } @inproceedings{LesensS00, author = {David Lesens and Hassen Sa{\"i}di}, title = {Abstraction of parameterized networks}, booktitle = {Infinity'97, Second International Workshop on Verification of Infinite State System}, series = {Electronic Notes in Theoretical Computer Science}, volume = {9}, publisher = {Elsevier Science Publishers}, editor = {Faron Moller}, year = {2000} } @article {KestenP00, AUTHOR = {Kesten, Y. and Pnueli, A.}, TITLE = {Control and Data Abstraction: The Cornerstones of Practical Formal Verification}, JOURNAL = {Software Tools for Technology Transfer}, VOLUME = {2}, YEAR = {2000}, NUMBER = {4}, PAGES = {328--342}, ISSN = {0890-5401}, MRCLASS = {68Q60 (68M15 68Q05 68Q68)}, MRNUMBER = {95c:68154}, MRREVIEWER = {}, } @incollection {AlurD90, AUTHOR = {Alur, R. and Dill, D.}, TITLE = {Automata for modeling real-time systems}, BOOKTITLE = {Automata, languages and programming}, PAGES = {322--335}, PUBLISHER = {Springer}, ADDRESS = {}, YEAR = {1990}, MRCLASS = {68Q05}, MRNUMBER = {1 076 829}, } @InProceedings{Alur99a, author = "R. Alur", year = "1999", title = "Timed Automata", booktitle = "Proc. 11th International Computer Aided Verification Conference", pages = "8--22", abstract = "Model checking is emerging as a practical tool for automated debugging of complex reative systems such as embedded controllers and network protocols (see [23] for a survey). Traditional techniques for model checking do not admit an explicit modeling of time, and are thus, unsuitable for analysis of real-time systems whose correctness depends on relative magnitudes of different delays. Consequently, timed automata [7] were introduced as a formal notation to model the behavior of real-time systems. Its definition provides a simple way to annotate state-transition graphs with timing constraints using finitely many real-valued clock variables. Automated analysis of timed automata relies on the construction of a finite quotient of the infinite space of clock valuations. Over the years, the formalism has been extensively studied leading to many results establishing connections to circuits and logic, and much progress has been made in developing verification algorithms, heuristics, and tools. This paper provides a survey of the theory of timed automata, and their role in specification and verification of real-time systems.", publisher = "Springer-Verlag", series = "Lecture Notes in Computer Science", volume = "1633", } @InProceedings{PnSh96, address = "New Brunswick, NJ, USA", author = "A. Pnueli and E. Shahar", booktitle = "Proceedings of the Eighth International Conference on Computer Aided Verification {CAV}", editor = "{Rajeev Alur} and {Thomas A. Henzinger}", key = "PnSh96", month = jul # "/" # aug, pages = "184--195", publisher = "Springer Verlag", series = "Lecture Notes in Computer Science", title = "A Platform Combining Deductive with Algorithmic Verification", volume = "1102", year = "1996", } @InProceedings{GPV94, author = "A. Gollu and A. Puri and P. Varaiya", title = "Discretization of timed automata", booktitle = "Proceedings of the 33rd IEEE conferene on decision and control", year = "1994", pages = "957--958", } @InProceedings{ABKM97, address = "Grenoble, France", author = "E. Asarin and M. Bozga and A. Kerbrat and O. Maler and M. Pnueli and A. Rasse", booktitle = "Hybrid and Real-Time Systems", editor = "O. Maler", key = "ABKM97", pages = "346--360", publisher = "Springer Verlag, LNCS 1201", title = "Data Structures for the Verification of Timed Automata", year = "1997", } @InProceedings{BDMOTY98, author = "M. Bozga and C. Daws and O. Maler and A. Olivero and S. Tripakis and S. Yovine", title = "Kronos: {A} Model-Checking Tool for Real-Time Systems", booktitle = "Proc.\ 10th International Conference on Computer Aided Verification, Vancouver, Canada", editor = "A. J. Hu and M. Y. Vardi", year = "1998", series = "Lecture Notes in Computer Science", volume = "1427", publisher = "Springer-Verlag", pages = "546--550", url = "http://www-verimag.imag.fr/~yovine/articles/kronos_cav98.html", } @Article{TOPLAS::AbadiL1994, title = "An Old-Fashioned Recipe for Real-Time", author = "Mart{\'\i}n Abadi and Leslie Lamport", journal = "ACM Transactions on Programming Languages and Systems", pages = "1543--1571", month = sep, year = "1994", volume = "16", number = "5", } @InProceedings{CONCUR::TasiranAKB1996, title = "Verifying Abstractions of Timed Systems", author = "Serdar Ta{\c{s}}{\i}ran and Rajeev Alur and Robert P. Kurshan and Robert K. Brayton", pages = "546--562", booktitle = "CONCUR~'96: Concurrency Theory, 7th International Conference", editor = "Ugo Montanari and Vladimiro Sassone", address = "Pisa, Italy", month = "26--29~" # aug, year = "1996", series = "Lecture Notes in Computer Science", volume = "1119", publisher = "Springer-Verlag", ISBN = "ISBN 3-540-61604-7", } @incollection {PJ99, AUTHOR = {P. A. Abdulla and B. Jonsson}, TITLE = {On the existence of network invariants for verifying parameterized systems}, BOOKTITLE = {Correct system design-recent insights and advances}, PAGES = {180--197}, PUBLISHER = {Springer}, ADDRESS = {}, YEAR = {1999}, MRCLASS = {68Q60}, MRNUMBER = {1 730 237}, } @InCollection{BolligL03, author = {Benedikt Bollig and Martin Leucker}, title = {Verifying Qualitative Properties of Probabilistic Programs}, booktitle = {Validation of Stochastic Systems}, publisher = {Springer}, year = 2004, volume = "2925", pages = "124--146", series = "Lecture Notes in Computer Science", url = "http://link.springer.de/link/service/series/0558/papers/", pdf = Documents # "Leucker/qualMC04.pdf.gz", postscript = Documents # "Leucker/qualMC04.ps.gz", abstract = "We present procedures for checking linear temporal logic and automata specifications of sequential and concurrent probabilistic programs. We follow two different approaches: For LTL and sequential probabilistic programs, our method proceeds in a tableau style fashion, while the remaining procedures are based on automata theory.", } @InProceedings{LeuckerSW03, author = {Martin Leucker and Rafal Somla and Michael Weber}, title = {Parallel Model Checking for {LTL}, {CTL{$^{\ast}$}} and {$L_{\mu}^2$}}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {89}, issue = {1}, publisher = {Elsevier Science Publishers}, editor = {Lubos Brim and Orna Grumberg}, year = {2003}, pdf = Documents # "Leucker/pdmc03.pdf.gz", postscript = Documents # "Leucker/pdmc03.ps.gz", } @InProceedings{GrinchteinL03, author = {Olga Grinchtein and Martin Leucker}, title = {Network Invariants for Real-time Systems}, booktitle = {5th International Workshop on Verification of Infinite-State Systems}, series = {Electronic Notes in Theoretical Computer Science}, volume = {98}, publisher = {Elsevier Science Publishers}, year = {2004}, pages = "57--74", pdf = Documents # "Leucker/infinity03.pdf.gz", postscript = Documents # "Leucker/infinity03.ps.gz", url = "http://www.sciencedirect.com/", } @TechReport{it:2003-039, author = {Therese Berg and Bengt Jonsson and Martin Leucker and Mayank Saksena}, title = {Insights to {A}ngluin's Learning}, institution = {Department of Information Technology, Uppsala University}, department = {Computer Systems}, year = 2003, number = {2003-039}, month = aug, abstract = {Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results. }, url = {http://www.it.uu.se/research/reports/2003-039/2003-039-nc.pdf}, pdf = Documents # "Berg/it2003.039.pdf.gz", postscript = Documents # "Berg/it2003.039.ps.gz", } @article{LeuckerNSW04, AUTHOR = {Martin Leucker and Thomas Noll and Perdita Stevens and Michael Weber}, TITLE = {Functional Programming Languages for Verification Tools: A Comparison of {ML} and {Haskell}}, JOURNAL = {Software Tools for Technology Transfer}, VOLUME = {7}, YEAR = {2005}, NUMBER = {2}, PAGES = {184--194}, ISSN = {0890-5401}, } @InProceedings{BolligLeucker03, title ="Model checking Probabilistic Distributed Systems", author ="Benedikt Bollig and Martin Leucker", booktitle ="Proceedings of the 8th Asian Computing Science Conference ({ASIAN'03})", pages ="291--304", address ="Mumbai, India", year =2003, month =dec, publisher ="Springer", series ="Lecture Notes in Computer Science", volume ="2896", abstract = "Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natural model for this kind of systems. To reason about these systems, we propose to use a product version of linear temporal logic (PLTL). The main result of the paper is a model-checking procedure for PPA and PLTL. With its help, it is possible to check qualitative properties of distributed systems automatically.", pdf = Documents # "Leucker/asian03.pdf.gz", postscript = Documents # "Leucker/asian03.ps.gz", url = "http://www.springerlink.com/media/g3t6cbhd4jcrng83ng86/Contributions/C/3/P/6/C3P6MDCKUFXABH8U_html/fulltext.html", } @InProceedings{BergJLS03, author = {Therese Berg and Bengt Jonsson and Martin Leucker and Mayank Saksena}, title = {Insights to {A}ngluin's Learning}, year = 2003, month = dec, abstract = {Among other domains, learning finite-state machines is important for obtaining a model of a system under development, so that powerful formal methods such as model checking can be applied. A prominent algorithm for learning such devices was developed by Angluin. We have implemented this algorithm in a straightforward way to gain further insights to practical applicability. Furthermore, we have analyzed its performance on randomly generated as well as real-world examples. Our experiments focus on the impact of the alphabet size and the number of states on the needed number of membership queries. Additionally, we have implemented and analyzed an optimized version for learning prefix-closed regular languages. Memory consumption is one major obstacle when we attempted to learn large examples. We see that prefix-closed languages are relatively hard to learn compared to arbitrary regular languages. The optimization, however, shows positive results. }, url = {http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4FFN49V-18-1&_cdi=13109&_user=616147&_orig=browse&_coverDate=02%2F01%2F2005&_sk=998819999&view=c&wchp=dGLbVlz-zSkzV&md5=1cd6a1fcf1599d96b97a2e45a181c0e5&ie=/sdarticle.pdf}, volume = "118", series = "Electronic Notes in Theoretical Computer Science", pages = "3--18", booktitle = "Proceedings of the International Workshop on Software Verification and Validation (SVV 2003)", pdf = Documents # "Berg/it2003.039.pdf.gz", postscript = Documents # "Berg/it2003.039.ps.gz", } @Article{ASB+95, author = "A. Aziz and V. Singhal and F. Balarin and R. K. Brayton", title = "It Usually Works: The Temporal Logic of Stochastic Systems", journal = "Lecture Notes in Computer Science", volume = "939", pages = "155ff", year = "1995", CODEN = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat May 11 13:45:32 MDT 1996", acknowledgement = ack-nhfb, } @Article{PnueliZuck86, author = "A. Pnueli and L. Zuck", title = "Verification of Multiprocess Probabilistic Protocols", journal = "Distributed Computing", volume = "1", year = "1986", pages = "53--72", note = "They present a temporal logic for proving liveness properties of probabilistic concurrent programs based on the notion of ``extreme fairness''.", } @InProceedings{Thomas02, author = {Wolfgang Thomas}, title = {Infinite Games and Verification (Extended Abstract of a Tutorial)}, booktitle = {Computer Aided Verification}, pages = {58--64}, year = 2003, volume = 2725, series = {Lecture Notes in Computer Science}, publisher = {Springer}, URL = "http://link.springer.de/link/service/series/0558/bibs/2404/24040058.htm; http://link.springer.de/link/service/series/0558/papers/2404/24040058.pdf", } @Book{FilarVrieze97, author = {J. Filar and K. Vrieze}, title = {Competitive Markov Decision Processes}, publisher = {Springer}, year = 1997 } @InProceedings{BouyerDMP03, author = {Patricia Bouyer and Deepak D'Souza and P. Madhusudan and Antoine Petit}, title = {Timed Control with Partial Observability}, booktitle = {Computer Aided Verification}, pages = {180--192}, year = 2003, volume = 2725, series = {Lecture Notes in Computer Science}, publisher = {Springer} } @Book{Baier98, author = {Christel Baier}, title = {On the algorithmic verification of probabilistic systems}, publisher = {Universit\"at Mannheim}, year = 1998, note = {Habilitation Thesis} } @Article{IPL::BaierK1998, title = "On the verification of qualitative properties of probabilistic processes under fairness constraints", author = "Christel Baier and Marta Kwiatkowska", pages = "71--79", journal = "Information Processing Letters", month = "29~" # apr, year = "1998", volume = "66", number = "2", references = "\cite{ICALP::AlurCD1991} \cite{DC::BaierK1998} \cite{ENTCS::BaierK1997} \cite{FOCS::CourcoubetisY1988} \cite{IC::GlabbeekSS1995} \cite{LICS::GlabbeekSST1990} \cite{FACS::HanssonJ1994} \cite{STOCCC::HartS1984} \cite{TOPLAS::HartSP1983} \cite{LICS::JonssonY1995} \cite{IC::LarsenS1991} \cite{CONCUR::LarsenS1992} \cite{ICALP::LehmannPS1981} \cite{IC::LehmannS1982} \cite{POPL::LichtensteinP1985} \cite{STOC::Pnueli1983} \cite{DC::PnueliZ1986} \cite{IC::PnueliZ1993} \cite{ACTAI::QueilleS1983} \cite{FACS::Tofts1994} \cite{FOCS::Vardi1985}", } @Article{BaierK98, author = {Christel Baier and Martha Kwiatkoswka}, title = {Model Checking for a Probabilistic Branching Time Logic with Fairness}, journal = {Distributed Computing}, year = 1998, volume = 11, number = 3, pages = {125--155} } @InProceedings{Bianco:1995:MCP, author = {A. Bianco and L. {De Alfaro}}, title = {Model checking of probabilistic and non-deterministic systems}, booktitle = {Proceedings of Foundations of Software Technology and Theoretical Computer Science}, pages = {499--513}, year = 1995, volume = 1026, series = {Lecture Notes in Computer Science} } @Book{DavPri:ilo, author = "B. A. Davey and H. A. Priestley", publisher = "Cambridge University Press", title = "Introduction to Lattices and Order", year = "2002", OPTedition = 2, } @PhdThesis{dAlf97a, author = {L. {de Alfaro}}, title = {Formal Verification of Probabilistic Systems}, school = {Stanford University}, year = 1997, note = {Technical report STAN-CS-TR-98-1601} } @InProceedings{STACS::Alfaro97, title = "Temporal Logics for the Specification of Performance and Reliability", author = "Luca de Alfaro", editor= "R. Reischuk and M. Morvan", booktitle = "14th Annual Symposium on Theoretical Aspects of Computer Science", address = "L{\"u}beck, Germany", year = "1997", series = "lncs", volume = "1200", publisher = "Springer", pages = "165--176", } @Article{HaJo94, author = {H.~Hansson and B.~Jonsson}, title = {A logic for reasoning about time and reliability}, journal = {Formal Aspects of Computing}, pages = {512--535}, volume = 6, year = {1994}, } @Book{Pute94, author = "Martin L. Puterman", title = "Markov Decision Processes: Discrete Stochastic Dynamic Programming", publisher = "John Wiley \& Sons, Inc.", year = "1994", address = "New York, NY", } @InProceedings{Jurd00, author = {M.~Jurdzinski}, title = {Small Progress for Solving Parity Games}, booktitle = {Proc.~STACS}, series = {LNCS}, volume = {1770}, pages = {290-301}, publisher = {Springer-Verlag}, year = {2000} } @InProceedings{VoegJurd00, author = {J.~V\"oge and M.~Jurdzinski}, title = {A Discrete Strategy Improvement Algorithm for Solving Parity Games}, booktitle = {Proc.~of the 12th International Conference on Computer Aided Verification (CAV)}, series = {LNCS}, volume = {1855}, pages = {202-215}, publisher = {Springer-Verlag}, year = {2000} } @InProceedings{CJH04, author = {K.~Chatterjee and M.~Jurdzinski and T.~Henzinger}, title = {Quantitative simple stochastic parity games}, booktitle = {Proceedings of the Annual Symposium on Discrete Algorithms (SODA)}, publisher = {SIAM}, year = {2004} } @InProceedings{CJH03, author = {K.~Chatterjee and M.~Jurdzinski and T.~Henzinger}, title = {Simple stochastic parity games}, booktitle = {Proceedings of the International Conference for Computer Science Logic (CSL)}, series = {Lecture Notes in Computer Science}, volume = {2803}, pages = {pp 100-113}, publisher = {Springer-Verlag}, year = {2003} } @InProceedings{JKH02, author = {M.~Jurdzinski and O.~Kupferman and T.~Henzinger}, title = {Trading Probability for Fairness}, booktitle = {Proceedings of the International Conference for Computer Science Logic (CSL)}, series = {Lecture Notes in Computer Science}, volume = {2471}, pages = {pp 292-305}, publisher = {Springer-Verlag}, year = {2003} } @InProceedings{dAHK98, author = {L.~de Alfaro and T.~Henzinger and O.~Kupferman}, title = {Concurrent reachability games}, booktitle = {Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS)}, publisher = {IEEE Computer Society Press}, pages = {pp. 564-575}, year = {1998} } @InProceedings{dAH00, author = {L.~de Alfaro and T.~Henzinger}, title = {Concurrent omega-regular games}, booktitle = {Proceedings of the 15th Annual Symposium on Logic in Computer Science (LICS)}, publisher = {IEEE Computer Society Press}, year = {2000}, pages = {pp. 141-154} } @InProceedings{EJ91, author = {E.A.~Emerson and C.S.~Jutla}, title = {Tree Automata, Mu-Calculus and Determinacy}, booktitle = {Proc.~32th Symp.~on Foundations of Computer Science (FOCS)}, publisher = {IEEE Computer Society Press}, year = {1991}, pages = {pp. 368-377} } @InProceedings{dAlf99, author = {L.~de Alfaro}, title = {Computing Minimum and Maximum Reachability Times in Probabilistic Systems}, booktitle = {Proc.~CONCUR'99}, series = {LNCS}, volume = {1664}, year = {1999}, pages = {pp. 66-81} } @Book{Der70, author = {C.~Derman}, title = {Finite-State Markovian Decision Processes}, publisher = {Academic Press}, year = {1970} } @InProceedings{dAM01, author = {L.~de Alfaro and R.~Majumdar}, title = {Quantitative Solution of omega-regular games}, booktitle = {Proc.~STOC'01}, publisher = {ACM Press}, year = {2001}, pages = {pp. 675-683} } @Article{AVW03, author = {A.~Arnold, A.~Vincent and I.~Walukiewicz}, title = {Games for Synthesis of Controllers with Partial Observations}, journal = {Theoretical Computer Science}, volume = {303}, pages = {7-34}, year = {2003} } @Article{Con92, author = {A.~Condon}, title = {The Complexity of Stochastic Games}, journal = {Information and Computation}, volume = {96}, pages = {203-224}, year = {1992} } @Article{Con93, author = {A.~Condon}, title = {On algorithms for simple stochastic games}, journal = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science}, volume = {13}, pages = {51-71}, year = {1993} } @InCollection{hromkovic01:_commun_protoc, author = "Juraj Hromkovi{\v c}", title = "Communication Protocols: An Exemplary Study of the Power of Randomness", booktitle = "Handbook on Randomized Computing", pages = "1048pp", publisher = "Kluwer Academic Publishers", year = "2001", editor = "P. Pardalos and S. Rajasekaran and J. Reif and J. Rolim", address = "Dordrecht, The Netherlands", language = "english", month = jun, ISBN = "0-7923-6959-9", } @Book{RandomizedComputing01, editor = "P. Pardalos and S. Rajasekaran and J. Reif and J. Rolim", title = "Handbook on Randomized Computing", publisher = "Kluwer Academic Publishers", address = "Dordrecht, The Netherlands", language = "english", month = jun, ISBN = "0-7923-6959-9", year = 2001, } @InProceedings{ClarkeEmeSis83, author = "E. M. Clarke and E. A. Emerson and A. P. Sistla", title = "Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: {A} Practical Approach", booktitle = "Conference Record of the Tenth Annual {ACM} Symposium on Principles of Programming Languages", address = "Austin, Texas", organization = "ACM SIGACT-SIGPLAN", month = jan # " 24--26,", year = "1983", pages = "117--126", } @InProceedings{HartSh84, author = "S. Hart and M. Sharir", title = "Probabilistic Temporal Logics for Finite and Bounded Models", pages = "1--13", booktitle = "{ACM} Symposium on Theory of Computing ({STOC} '84)", month = apr, publisher = "ACM Press", address = "Baltimore, USA", year = "1984", ISBN = "0-89791-133-4", } @Article{IC::LehmannS1982, title = "Reasoning with Time and Chance", author = "Daniel Lehmann and Saharon Shelah", pages = "165--198", journal = "Information and Control", month = jun, year = "1982", volume = "53", number = "3", references = "popl::Ben-AriMP1981, stoc::EmersonH1982, stoc::FeldmanH1982, popl::GabbayPSS1980, stoc::HalpernR1983, popl::HartSP1982, jcss::Kozen1981, popl::Lamport1980, sicomp::Lehmann1982, popl::LehmannR1981, tcs::Pnueli1981, jcss::Rabin1982, actai::Rabin1982, stoc::Reif1980, stoc::SistlaC1982:159, sicomp::SolovayS1977", references = "\cite{POPL::Ben-AriMP1981} \cite{STOC::EmersonH1982} \cite{STOC::FeldmanH1982} \cite{POPL::GabbayPSS1980} \cite{STOC::HalpernR1983} \cite{POPL::HartSP1982} \cite{JCSS::Kozen1981} \cite{POPL::Lamport1980} \cite{SICOMP::Lehmann1982} \cite{POPL::LehmannR1981} \cite{TCS::Pnueli1981} \cite{JCSS::Rabin1982} \cite{ACTAI::Rabin1982} \cite{STOC::Reif1980} \cite{STOC::SistlaC1982} \cite{SICOMP::SolovayS1977}", } @InProceedings{LehmanR81, author = {D. Lehman and M. O. Rabin}, title = {On the Advantage of Free Choice: A Fully Symmetric and Fully Distributed Solution to the Dining Philosophers Problem }, booktitle = {Proceedings of 10th ACM Symposium of Principles of Programming Languages}, pages = {133-138}, year = 1981, address = {Williamsburg} } @InProceedings{STOC::Pnueli1983, title = "On the Extremely Fair Treatment of Probabilistic Algorithms", author = "Amir Pnueli", pages = "278--290", booktitle = "Proceedings of the Fifteenth Annual {ACM} Symposium on Theory of Computing", month = "25--27 " # apr, year = "1983", address = "Boston, Massachusetts", } @Article{IC::Wolper1983, title = "Temporal Logic Can Be More Expressive", author = "Pierre Wolper", pages = "72--99", journal = "Information and Control", month = jan # "/" # feb, year = "1983", volume = "56", number = "1/2", references = "FOCS::HarelKP1980, FOCS::HarelPS1981, FOCS::HalpernR1981, FOCS::Pnueli1977, STOC::SistlaC1982, STOC::Streett1981, popl::Ben-AriMP1981, jcss::CohenG1977, jcss::FischerL1979, popl::GabbayPSS1980, tcs::KozenP1981, jcss::Savitch1970, popl::Wolper1982, icalp::EmersonC1980", references = "\cite{FOCS::HarelKP1980} \cite{FOCS::HarelPS1981} \cite{FOCS::HalpernR1981} \cite{FOCS::Pnueli1977} \cite{STOC::SistlaC1982} \cite{STOC::Streett1981} \cite{POPL::Ben-AriMP1981} \cite{JCSS::CohenG1977} \cite{JCSS::FischerL1979} \cite{POPL::GabbayPSS1980} \cite{TCS::KozenP1981} \cite{JCSS::Savitch1970} \cite{POPL::Wolper1982} \cite{ICALP::EmersonC1980}", } @TechReport{BolligLeucker04TR02, author = "Benedikt Bollig and Martin Leucker", title = "Message-Passing Automata are expressively equivalent to {EMSO} logic", institution = "RWTH Aachen", year = "2004", number = "AIB-2004-02", month = feb, url = "http://aib.informatik.rwth-aachen.de/2004/2004-02.ps.gz", postscript = Documents # "Leucker/2004-02.ps.gz", pdf = Documents # "Leucker/2004-02.pdf.gz", abstract = "We study the expressiveness of finite message-passing automata with a priori unbounded channels and show them to capture exactly the class of MSC languages that are definable in existential monadic second-order logic interpreted over MSCs. Moreover, we prove the monadic quantifier-alternation hierarchy over MSCs to be infinite and conclude that the class of MSC languages accepted by message-passing automata is not closed under complement. Furthermore, we show that satisfiability for (existential) monadic seconder-order logic over MSCs is undecidable.", } @InProceedings{BGLBC04, author = "Christel Baier and Marcus Gr{\"o}{\ss}er and Martin Leucker and Benedikt Bollig and Frank Ciesinski", title = "Controller Synthesis for Probabilistic Systems", booktitle = "Proceedings of the IFIP International Conference on Theoretical Computer Science, IFIP TCS2004", pages = "", year = "2004", volume = "", series = "", month = aug, publisher = "Kluwer", note = "to appear, link is to extended version", url = "http://web.informatik.uni-bonn.de/I/baier/papers/BGLBC.pdf", } @InProceedings{BarnatBC02, author = {J. Barnat and L. Brim and I. \v{C}ern\'{a}}, title = {Property Driven Distribution of Nested {DFS}}, booktitle = {VCL 2002: The Third International Workshop on Verification and Computational Logic, Pittsburgh PA, October 5, 2002 (held at the PLI 2002 Symposium)}, pages = {??--??}, year = {2002}, } @InProceedings{BolligLeucker04, author = {Benedikt Bollig and Martin Leucker}, title = {Message-Passing Automata are expressively equivalent to {EMSO} Logic}, booktitle = {Proceedings of the 15th International Conference on Concurrency Theory (CONCUR'04)}, year = 2004, series = {Lecture Notes in Computer Science}, address = {London, UK}, month = aug, publisher = {Springer}, url = "http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=3170&spage=146", pdf = Documents # "Leucker/concur04.pdf.gz", } @InProceedings{GrinchteinJL04, author = {Olga Grinchtein and Bengt Jonsson and Martin Leucker}, title = {Learning of Event-Recording Automata}, booktitle = {Proceedings of the Joint Conferences {FORMATS} and {FTRTFT}}, year = 2004, series = {Lecture Notes in Computer Science}, month = sep, volume = "3253", abstract = "We extend Angluin's algorithm for on-line learning of regular languages to the setting of timed systems. We consider systems that can be described by a class of deterministic event-recording automata. Our algorithm learns a description by asking a sequence of membership queries (does the system accept a given timed word?) and equivalence queries (is a hypothesized description equivalent to the correct one?). In the constructed description, states are identified by sequences of symbols; timing constraints on transitions are learned by adapting algorithms for learning hypercubes. The number of membership queries is polynomially in the minimal zone graph and in the biggest constant of the automaton to learn.", postscript = Documents # "Leucker/formats04.ps.gz", pdf = Documents # "Leucker/formats04.pdf.gz", } @INPROCEEDINGS{CoCo:abstract, Author = "P. Cousot and R. Cousot", Title = "Abstract Interpretation: A Unified Model for Static Analysis of Programs by Construction or Approximation of Fixpoints", booktitle = "Proc.\ \Nth{4} ACM Symp.\ on Principles of Programming Languages", Year = "1977", Pages = "238-252" } @INPROCEEDINGS{Dams:Grumberg:Gerth:Abstraction, Author = "D. Dams and O. Grumberg and R. Gerth", Title = "Abstract Interpretation of Reactive Systems: Abstractions Preserving $\forall\mbox{CTL}^*,\exists\mbox{CTL}^* \mbox{ and }\mbox{CTL}^*$", booktitle = "Proc. IFIP working conference on Programming Concepts, Methods and Calculi (PROCOMET'94)", Year = "1994", Pages="573-592" } @INPROCEEDINGS{GS:pvs, Author = "S. Graf and H. Saidi", Title = "Construction of Abstract State Graphs with {PVS}", booktitle = CAV97, Volume = 1254, Publisher = {Springer-Verlag}, Year = 1997, Pages="72-83", Address = "Haifa, Israel" } @INPROCEEDINGS{DDP:abstraction, Author = "S. Das and D.L. Dill and S. Park", Title = "Experience with Predicate Abstraction", booktitle = {CAV99}, Series = {LNCS}, Volume = 1633, Year = 1999} @InProceedings{Bensalem:abstraction, author = "S. Bensalem and Y. Lakhnech and S. Owre", title = "Computing Abstractions of Infinite State Systems Automatically and Compositionally", editor = "Alan J. Hu and Moshe Y. Vardi", volume = 1427, series = "Lecture Notes in Computer Science", pages = "319-331", booktitle = "Computer Aided Verification", year = 1998, publisher = "Springer-Verlag" } @INPROCEEDINGS{CoUr:abstractions, Author = "M.A. Colon and T.E. Uribe", Title = " Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures", booktitle = CAV98, series= LNCS, publisher = "Springer-Verlag", volume=1427, pages = "293-304", Year = 1998 } @INPROCEEDINGS{SaSh:abstract, Author = "H. Saidi and N. Shankar", Title = "Abstract and Model Check while you Prove", booktitle = CAV99, Series = LNCS, Volume = 1633, Year = 1999 } @ARTICLE{J94, Author="B. Jonsson", Title="Compositional specification and verification of distributed systems", Journal=TOPLAS, Volume=16, Number=2, Year=1994, Pages="259--303" } @INPROCEEDINGS{ScBlMa:outlines, Author = "F.~B. Schneider and B. Bloom and K. Marzullo", Title = "Putting Time Into Proof Outlines", Editor = "{de Bakker} and Huizing and {de Roever} and Rozenberg", Booktitle = "Real-Time: Theory in Practice", Year = 1992, Pages="618--639", Series = LNCS, Volume = 600 } @Article{IC:KVW, title = "Module Checking", author = "O. Kupferman and M. Vardi and P. Wolper", pages = "322--344", journal = "Information and Computation", year = "2001", volume = "164", number = "2", references = "\cite{JACM::BerryL1979} \cite{JACM::BrookesHR1984} \cite{JACM::CastellaniH1989} \cite{LICS::DeganoNM1988} \cite{LICS::DeganoMM1989}", } @InProceedings{OuaknineW03, author = {Jo{\"e}l Ouaknine and James Worrell}, title = {Revisiting Digitization, Robustness, and Decidability for Timed Automata}, booktitle = {Proceedings of the \Nth{18} Annual {IEEE} Symposium on Logic in Computer Science {(LICS'03)}}, year = 2003, publisher = {IEEE Computer Society} } @InProceedings{LeuckerHL04, author = {Fredrik Holm{\'e}n and Martin Leucker and Marcus Lindstr{\"o}m}, title = {{UppDMC} -- A Distributed Model Checker for Fragments of the {$\mu$}-calculus}, booktitle = {Proceedings of the $3rd$ Workshop on Parallel and Distributed Methods for Verification}, volume = {128/3}, series = {Electronic Notes in Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Lubos Brim and Martin Leucker}, year = {2004}, pdf = Documents # "Leucker/pdmc04.pdf.gz", postscript = Documents # "Leucker/pdmc04.ps.gz", abstract = " We present UppDMC, a distributed model-checking tool. It is tailored for checking finite-state systems and mu-calculus specifications with at most one alternation of minimal and maximal fixed-point operators. This fragment is also known as LmuTwo. Recently, efficient game-based algorithms for this logic have been outlined. We describe the implementation of these algorithms within UppDMC and study their performance on practical examples. Running UppDMC on a simple workstation cluster, we were able to check liveness properties of the largest examples given in the VLTS Benchmark Suite, for which no answers were previously known.", } @InProceedings{GrinchteinJL04b, author = {Olga Grinchtein and Bengt Jonsson and Martin Leucker}, title = {Inference of Timed Transition Systems}, booktitle = {6th International Workshop on Verification of Infinite-State Systems}, series = {Electronic Notes in Theoretical Computer Science}, volume = {??}, publisher = {Elsevier Science Publishers}, year = {2004}, pdf = Documents # "Leucker/infinity04.pdf.gz", postscript = Documents # "Leucker/infinity04.ps.gz", note = "to appear", abstract = "We extend Angluin's algorithm for on-line learning of regular languages to the setting of timed transition systems. More specifically, we describe a procedure for inferring systems that can be described by event-recording automata by asking a sequence of membership queries (does the system accept a given timed word?) and equivalence queries (is a hypothesized description equivalent to the correct one?). In the inferred description, states are identified by sequences of symbols together with timing information. The number of membership queries is polynomially in the region graph and in the biggest constant of the automaton to learn.", } @Article{MorganIver99, author = "C. Morgan and A. McIver", title = "{pGCL}: Formal reasoning for random algorithms", journal = {South African Computer Journal}, year = "1999", url = "citeseer.nj.nec.com/morgan99pgcl.html" } @InProceedings{BCG04, author = "C. Baier and F. Ciesinski and M. Gr{\"o}{\ss}er", title = "PROBMELA: a modeling language for communicating probabilistic systems", booktitle = "Proc.~MEMOCODE", year = "2004", } @InProceedings{dAFHMS03, author = "L.~de Alfaro and M.~Faella and T.~Henzinger and R.~Majumdar and M.~Stoelinga", title = "The Element of Surprise in Timed Games", booktitle = "Proc.~CONCUR", series = "Lecture Notes in Computer Science", volume = "2761", pages = "144-158", year = "2003", } @techreport{ antoniotti95supervisor, author = "M. Antoniotti and B. Mishra", title = "The Supervisor Synthesis Problem for Unrestricted {CTL} is {NP}-complete", number = "TR1995-707", year = "1995" } @Article{AspPlTar79, title = "A linear-time algorithm for testing the truth of certain quantified boolean formulas", author = "B. Aspvall and M. F. Plass and R. E. Tarjan", pages = "121--123", journal = "Information Processing Letters", year = "1979", volume = "8", number = "3" } @InProceedings{mitchell:probabilistic-polynomial-time, author = "John C. Mitchell", title = "Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis", booktitle = "Programming Languages and Systems: Proceedings of the 10th European Symposium on Programming ({ESOP} 2001), Held as Part of the Joint European Conferences on Theory and Practice of Software ({ETAPS} 2001), (Genova, Italy, April 2001)", year = "2001", editor = "David Sands", volume = "2028", series = "LNCS", publisher = "Springer", pages = "23--29", } @InProceedings{GrumbergLLS05, author = {Orna Grumberg and Martin Lange and Martin Leucker and Sharon Shoham}, title = {\emph{Don't know} in the $\mu$-calculus}, booktitle = {Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05)}, year = 2005, series = {Lecture Notes in Computer Science}, volume = "3385", publisher = {Springer}, postscript = Documents # "Leucker/vmcai05.ps.gz", pdf = Documents # "Leucker/vmcai05.pdf.gz" } @InProceedings{BHV00, author = "G. Behrmann and T. S. Hune and F. W. Vaandrager", booktitle = "Proceedings of the 12th International Conference on Computer Aided Verification", editor = "E. A. Emerson and A. P. Sistla", year = "2000", series = "Lecture Notes in Computer Science", volume = "1855", publisher = "Springer-Verlag", title = "Distributed Timed Model Checking --- How the Search Order Matters", pages = "216--231", } @InProceedings{LerdaSisto00, author = {Flavio Lerda and Riccardo Sisto}, title = "Distributed-Memory Model Checking with {SPIN}", booktitle = {Proceedings of the 5th International {SPIN} Workshop}, pages = {22--39}, year = 1999, volume = 1680, series = {Lecture Notes in Computer Science}, publisher = {Springer}, abstract = "The main limiting factor of the model checker SPIN is currently the amount of available physical memory. This paper explores the possibility of exploiting a distributed-memory execution environment, such as a network of workstations interconnected by a standard LAN, to extend the size of the veri cation problems that can be successfully handled by SPIN. A distributed version of the algorithm used by SPIN to verify safety properties is presented, and its compatibility with the main memory and complexity reduction mechanisms of SPIN is discussed. Finally, some preliminary experimental results are presented.", URL = "http://citeseer.ist.psu.edu/417949.html; http://netlib.bell-labs.com/netlib/spin/ws99a/distr.ps.gz", } @InProceedings{GruHeySch03, author = "Grumberg and Heyman and Schuster", title = "A Work-Efficient Distributed Algorithm for Reachability Analysis", booktitle = "CAV: International Conference on Computer Aided Verification", year = "2003", } @InProceedings{GroceVisser02, author = {Alex Groce and Willem Visser}, title = {Heuristic Model Checking for Java Programs}, booktitle = {Proceedings of the 9th International {SPIN} Workshop}, year = 2002, volume = 2318, series = {Lecture Notes in Computer Science}, publisher = {Springer}, abstract = "This paper describes the addition of support for heuristic (or directed) search strategies to JavaPathFinder (JPF), an explicit state model checker for Java bytecode that uses a custom-made Java Virtual Machine (JVM)", URL = "http://citeseer.ist.psu.edu/508003.html; http://netlib.bell-labs.com/netlib/spin/ws02/groce.pdf", } @InProceedings{RangarajanC04, author = {Murali Rangarajan and Darren Cofer}, title = {Model-Checking Complex Software -- A Memory Perspective}, booktitle = {Radical Innovations of Software and Systems Engineering in the Future: 9th International Workshop, {RISSEF 2002}}, series = {Lecture Notes in Computer Science}, publisher = {Springer}, pages = {283--296}, year = 2004, volume = 2941, abstract = "In recent times, there has been growing interest in model checking software systems. Such efforts bring into focus the memory constraints of model checking approaches. In this paper, we present our results from the analysis (at the source code level) of a real-time operating system using the Spin model checker and explain our efforts to understand the reasons for the extremely large state space. Our studies indicate that even hand-optimized models suffer from memory constraints, thereby indicating the need for other approaches that break the problem into smaller pieces. ", } @InProceedings{BellHaverkort02, booktitle = {Proceedings of the 1st Workshop on Parallel and Distributed Methods for Verification}, title = "Sequential and Distributed Model Checking of Petri Net Specifications", author = "Alexander Bell and Boudewijn R. Haverkort", year = 2002, series = "Electronic Notes in Theoretical Computer Science", volume = 68, abstract = "In this paper we present algorithms for model checking CTL over systems specified as Petri nets. We present sequential as well as distributed model checking algorithms. The algorithms rely on an explicit representation of the system state space, but do not require the transition relation to be explicitly available; it is recomputed whenever required. This approach allows us to model check very large systems, with hundreds of millions of states, in a fast and efficient way. Furthermore, our distributed algorithms scale very well, as they show efficiencies in the range of 80 to 100\%.", URL = "http://citeseer.ist.psu.edu/545043.html; ftp://ftp-lvs.informatik.rwth-aachen.de/pub/papers/2002/pdmc02.pdf", } @InProceedings{Weise97, booktitle = {Proceedings of the 3rd International {SPIN} Workshop}, title = "An incremental formal semantics for {PROMELA}", author = "Carsten Weise", year = 1997, abstract = "An approach to a formal semantics definition for PROMELA is presented. The approach uses SOS rules to define a labeled transition system model for a PROMELA program. The approach is a bottom-up, incremental approach with three basic steps (declarations, single processes, parallel processes). PROMELA before version 2.0 is treated nearly entirely. Especially assertions, never claims, and correctness conditions are discussed.", URL = "http://citeseer.ist.psu.edu/111317.html; ftp://ftp.netlib.org/spin/ws97/weise.ps.Z", } @TechReport{NH96, title = "Outline for an Operational-Semantics Definition of {PROMELA}", author = "Gerard J. Holzmann and V. Natarajan", year = "1996", month = "July", institution = "Bell Laboratories", citeseer-isreferencedby = "oai:CiteSeerPSU:238335; oai:CiteSeerPSU:282210; oai:CiteSeerPSU:13471; oai:CiteSeerPSU:239562; oai:CiteSeerPSU:341505; oai:CiteSeerPSU:366176", annote = "The Pennsylvania State University CiteSeer Archives", language = "en", oai = "oai:CiteSeerPSU:147916", rights = "unrestricted", subject = "Gerard J. Holzmann,V. Natarajan Outline for an Operational-Semantics Definition of PROMELA", URL = "http://citeseer.ist.psu.edu/147916.html; ftp://netlib.bell-labs.com/netlib/spin/ws96/Na.ps.Z", } @InProceedings{BergGJLRS05, author = {Therese Berg and Olga Grinchtein and Bengt Jonsson and Martin Leucker and Harald Raffelt and Bernhard Steffen}, title = {On the Correspondence between Conformance Testing and Regular Inference}, booktitle = {Fundamental Approaches to Software Engineering, FASE'05}, pages = {175--189}, year = 2005, editor = {Maura Cerioli}, volume = 3442, series = {Lecture Notes in Computer Science}, publisher = {Springer}, } @Article{BolligLeucker05, author = {Benedikt Bollig and Martin Leucker}, title = {Message-Passing Automata are expressively equivalent to {EMSO} Logic}, journal = {Theoretical Computer Science}, year = {2005}, OPTkey = {}, OPTvolume = {}, OPTnumber = {}, OPTpages = {}, OPTmonth = {}, OPTnote = {Special Issue of CONCUR'04, accepted}, OPTannote = {} } @Book{BroyJKLP05, editor = {Manfred Broy and Bengt Jonsson and Joost-Pieter Katoen and Martin Leucker and Alexander Pretschner}, title = {Model-based Testing of Reactive Systems}, publisher = {Springer}, year = 2005, series = {Lecture Notes in Computer Science}, volume = {3472}, note = {to appear} } @InBook{ColinM05, author = {S{\'e}verine Colin and Leonardo Mariani}, title = {Run-Time Verification}, chapter = 18, crossref = "BroyJKLP05", } @MastersThesis{Dietl05, author = {Tobias Dietl}, title = {{Diagnose von Software-Komponenten im Automobil}}, school = {Technische Universit{\"a}t M{\"u}nchen}, year = 2005 } @Book{GraedelTW02, title = {Automata, Logics and Infinite Games}, publisher = {Springer}, year = 2002, editor = {Erich Gr{\"a}del and Wolfgang Thomas and {Th}omas Wilke}, volume = "2500", series = "Lecture Notes in Computer Science", url = "http://link.springer.de/link/service/series/0558/papers/2500/", } @InCollection{BiereCCSZ03, author = {A. Biere and A. Cimatti and E. Clarke and O. Strichman and Y. Zhu}, title = {Bounded Model Checking}, publisher = {Academic press}, year = 2003, volume = 58, series = {Advances in Computers} } @Article{Gastin:2001:FLB, author = "Paul Gastin and Denis Oddoux", title = "Fast {LTL} to {B{\"u}chi} Automata Translation", journal = "Lecture Notes in Computer Science", volume = "2102", pages = "53--??", year = "2001", CODEN = "LNCSD9", ISSN = "0302-9743", bibdate = "Sat Feb 2 13:05:02 MST 2002", URL = "http://link.springer-ny.com/link/service/series/0558/bibs/2102/21020053.htm; http://link.springer-ny.com/link/service/series/0558/papers/2102/21020053.pdf", acknowledgement = ack-nhfb, } @Article{FriWil02, author = "Fritz and Wilke", title = "State Space Reductions for Alternating Buchi Automata", journal = "FSTTCS: Foundations of Software Technology and Theoretical Computer Science", volume = "22", year = "2002", } @Article{BaaderHLW03, author = {Franz Baader and Jan Hladik and Carsten Lutz and Frank Wolter}, title = {From Tableaux to Automata for Description Logics}, journal = {Fundamenta Informaticae}, year = 2003, volume = 57, number = {2--4}, pages = {247--279} } @Proceedings{BrimLeucker05, editor = {Lubos Brim and Martin Leucker}, title = {Proceedings of the $3rd$ Workshop on Parallel and Distributed Methods for Verification}, volume = {128/3}, series = {Electronic Notes in Computer Science}, publisher = {Elsevier Science Publishers}, editor = {Lubos Brim and Martin Leucker}, year = {2005}, url = "http://www.sciencedirect.com/science?_ob=IssueURL&_tockey=%23TOC%2313109%232005%23998719996%23587069%23FLP%23Volume_128,_Issue_3,_Pages_1-138_(19_April_2005)%2BMProceedings_of_the_3rd_International_Workshop_on_Parallel_and_Distributed_Methods_in_Verification_(PDMC_2004)%2BM04_September_2004%2BMEdited_by_L._Brim%3B_M._Leucker&_auth=y&view=c&_acct=C000032324&_version=1&_urlVersion=0&_userid=616147&md5=adaf4b39107a0042ebe24d5cd8188eb0", } @book{lsvmcbook01, author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain and Laroussinie, Fran{\c c}ois and Petit, Antoine and Petrucci, Laure and Schnoebelen, {\relax Ph}ilippe}, publisher = {Springer}, title = {Systems and Software Verification. {M}odel-Checking Techniques and Tools}, url = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8}, year = {2001}, } @Book{Peled01, author = {Doron Peled}, title = {Software Reliability Methods}, publisher = {Springer}, year = 2001 }