IEEE CONTROL SYSTEMS SOCIETY TECHNICAL COMMITTEE ON DISCRETE EVENT SYSTEMS Newsletter......................................................March, 2005 Editor: Ryan J. Leduc Chair, IEEE CSS Technical Committee on DES Dept. of Computing and Software McMaster University 1280 Main Street West Hamilton, Ontario Canada L8S 4K1 Phone: (905) 525-9140 Ext. 27962 Fax: (905) 524-0340 e-mail: leduc@mcmaster.ca WWW: http://www.cas.mcmaster.ca/~leduc/ DESTC Web Page: http://www.cas.mcmaster.ca/destc/ To subscribe/unsubscribe or submit news items and articles to this newsletter, send e-mail to: destcsubm@cas.mcmaster.ca _._________________________________________________________________________._ Contents: 1. Editorial 2. Announcements 2.1 Call for Submissions to DES Newsletter. 2.2 DES Technical Committee Meeting at ACC'05. 2.3 Central List of DES Researchers. 3. Books 3.1 "VERIFICATION OF REACTIVE SYSTEMS," by Klaus Schneider. 4. Conferences 4.1 Workshops on Discrete Event Systems (WODES'06), Ann Arbor, USA, July 10-12, 2006. 4.2 Workshop on Control of Hybrid and Discrete Event Systems, Miami, Florida, USA, June 21, 2005. _._________________________________________________________________________._ Editorial _._________________________________________________________________________._ Welcome to the newsletter of the IEEE Control Systems Technical Committee Group on Discrete Event Systems! See http://www.cas.mcmaster.ca/destc/ for information on the DESTC. Notice the delimiter between articles/contributions in this newsletter. If you are using an editor to read this article, you can go directly to the delimiter by searching for the string "_.__" (underscore, period, underscore, underscore). This feature is useful for quickly skipping to the next item. Personal note from the editor: As of January 1, 2005, I am the new chairman of the IEEE DES technical committee. My first task will be to revive the newsletter which I hope to send out every 3-4 months or so, depending on how much news there is. Please submit relevant news items and articles for the newsletter, and pass the newsletter on to anyone who you think would be interested. As this list is quite out of date, many people who used to be on the mailing list have changed their e-mail addresses, and thus would not receive this message. Please see below for more details and upcoming activities. I apologize for the sparseness of content, but the newsletter is only just starting up again. _._________________________________________________________________________._ Announcements _._________________________________________________________________________._ Contributed by: Ryan Leduc CALL FOR SUBMISSIONS TO DES NEWSLETTER If you have any news or announcements relevant to DES researchers, please send the info to: destcsubm@cas.mcmaster.ca Examples of contributions include announcements on: * Conferences * Workshops * Special sessions * Publications * Courses * Personals * Job opportunities and positions * Web sites The announcements should be submitted as plain text (please no HTML). Previous versions of the newsletter can be found at http://www.cas.mcmaster.ca/destc/ and can be used as a guide on what information to include. _._________________________________________________________________________._ Contributed by: Ryan Leduc DES TECHNICAL COMMITTEE MEETING AT ACC'05 There will be a meeting of the IEEE Control Systems Technical Committee Group on Discrete Event Systems at the 2005 American Control Conference (http://www.ee.washington.edu/conf/acc2005/) in Portland, Oregon, on Friday, June 10, 2005, from 1:30-2:30pm. The room number is to be announced. If you are interested in helping out with the committee's activities and will be at the ACC'05, please send me an e-mail (destc@cas.mcmaster.ca) to let me know to expect you. How much you choose to participate is always up to you. Whether you simply give us the benefit of your experience and wisdom during discussions, or take a more active role in organizing activities, you will be equally welcome. If you are interested in participating but will not be at the ACC'05, please send me an e-mail to let me know. I'll let you know afterwards what took place. _._________________________________________________________________________._ Contributed by: Ryan Leduc CENTRAL LIST OF DES RESEARCHERS In the interest of facilitating communication amongst DES researchers, I will be setting up a list of DES researchers linked to the DESTC website (http://www.cas.mcmaster.ca/destc/). The goal is to make it easy to find other DES researchers, and to quickly get an idea of what their research interests are. The list is purely for information and contact purposes. To have your name added, please send an email to destcsubm@cas.mcmaster.ca with subject: CLDESR In the e-mail, please provide: * Your name. * Position (ie. professor, student, researcher etc). * Name of your organization. * E-mail address or link to web page or phone number (web page link preferred, assuming the web page has full contact information). * A one line summary of your research interests. _._________________________________________________________________________._ Books _._________________________________________________________________________._ Contributed by: Klaus Schneider BOOK ANNOUNCEMENT VERIFICATION OF REACTIVE SYSTEMS Klaus Schneider Springer Verlag, 2003, ISBN 3-540-00296-0 http://rsg.informatik.uni-kl.de/research/VeReSys/index.html * This book considers the most popular logics for specification and verification of reactive systems. In particular, the relationships and verification procedures of the propositional mu-calculus, omega-automata, temporal logics, and (monadic) predicate logics are covered in full detail. The book has a special emphasis on algorithms that are listed as detailed pseudo-code programs. This makes the book particularly useful for those who want to implement or understand modern verification procedures. Most results are given with detailed proofs, so that the presentation is self-contained. This book is targeted to advanced students, lecturers, and researchers in the area. * Course materials (slides and exercises) based on the book will be made available before/during the next summer term. * A public domain verification tool (Averest) that implements some of the algorithms is available under http://www.averest.org * Further information, a free chapter, and updated sections are available under http://rsg.informatik.uni-kl.de/research/VeReSys/index.html TABLE OF CONTENTS 1 Introduction 1.1 Formal Methods in System Design 1.1.1 General Remarks and Taxonomy 1.1.2 Classification of Formal Methods 1.1.3 Classification of Systems 1.2 Genealogy of Formal Verification 1.2.1 Early Beginnings of Mathematical Logic 1.2.2 Automated Theorem Proving 1.2.3 Beginnings of Program Verification 1.2.4 Dynamic Logics and Fixpoint Calculi 1.2.5 Temporal Logics 1.2.6 Decidable Theories and omega-Automata 1.2.7 Summary 1.3 Outline of the Book 2 A Unified Specification Language 2.1 Kripke Structures as Formal Models of Reactive Systems 2.1.1 Simulation and Bisimulation of Kripke Structures 2.1.2 Quotient Structures 2.1.3 Products of Kripke Structures 2.2 Syntax of the Specification Logic L_spec 2.3 Semantics of the Specification Logic L_spec 2.4 Normal Forms 3 Fixpoint Calculi 3.1 Partial Orders, Lattices and Fixpoints 3.2 The Basic 5-Calculus 3.3 Monotonicity of State Transformers 3.4 Model Checking of the Basic 5-Calculus 3.4.1 A Naive Model Checking Procedure 3.4.2 Optimization by the Alternation Depth 3.5 Vectorized 5-Calculus 3.5.1 State Transformers of Vectorized Fixpoint Expressions 3.5.2 Decomposing Equation Systems 3.5.3 Model Checking Vectorized Fixpoint Expressions 3.5.4 Comparing Basic and Vectorized 5-Calculus Model Checking 3.5.5 Dependency-Triggered Evaluations 3.5.6 The Cleaveland-Steffen Algorithm 3.6 Reducing the Alternation Depth w.r.t. Structures 3.7 Computing Fair States and Fair Paths (Counterexamples) 3.7.1 Kripke Structures with Fairness Constraints 3.7.2 SCC Partitioning by Depth-First Traversals 3.7.3 SCC Partitioning by Breadth-First Traversals 3.7.4 Fully Symbolic Computation of Fair States 3.8 Final Remarks on Completeness and Expressiveness 3.8.1 Bisimilarity and the Future Fragment 3.8.2 Relationship to omega-Tree Automata and Games 3.8.3 Dynamic Logic 4 Finite Automata 4.1 Regular Languages, Regular Expressions and Automata 4.2 The Logic of Automaton Formulas 4.3 Boolean Closure 4.4 Converting Automaton Classes 4.5 Determinization and Complementation 4.5.1 The Rabin-Scott Subset Construction 4.5.2 Determinization of NDetF 4.5.3 Determinization of NDetG 4.5.4 Determinization of NDetFG 4.5.5 Reducing NDetGF to DetRabin 4.6 The Hierarchy of omega-Automata and the Borel Hierarchy 4.7 Automata and Monoids 4.7.1 Finite Semigroups and Monoids 4.7.2 Automata and Their Monoids 4.8 Decision Procedures for omega-Automata 4.8.1 Flattening omega-Automata 4.8.2 Translating omega-Automata Model Checking to 5-Calculus Model Checking 4.8.3 Translating Automata to Vectorized 5-Calculus 5 Temporal Logics 5.1 Introduction 5.2 Branching Time Logics Sublanguages of CTL 5.2.1 CTL, LTL and CTL 5.2.2 Adding Syntactic Sugar to CTL 5.3 Translating Temporal Logics to the 5-Calculus 5.3.1 CTL and FairCTL as Fragments of the 5-Calculus 5.3.2 CTL2 as a Fragment of the 5-Calculus 5.3.3 Eliminating Quantified Boolean Expressions 5.3.4 Adding Path Quantifiers 5.3.5 Translating LeftCTL* to Vectorized 5-Calculus 5.4 Translating Temporal Logics to omega-Automata 5.4.1 The Basic Translation from LTLp to NDetStreett 5.4.2 Exploitation of Monotonicity 5.4.3 Borel Classes of Temporal Logic 5.4.4 Reducing Temporal Borel Classes to Borel Automata 5.4.5 Reductions to CTL/LeftCTL. Model Checking 5.5 Completeness and Expressiveness of Temporal Logic 5.5.1 Noncounting Automata and Temporal Logic 5.5.2 Completeness of the Borel Classes 5.5.3 Completeness of the Future Fragments 5.6 Complexities of the Model Checking Problems 5.7 Reductions by Simulation and Bisimulation Relations 6 Predicate Logic 6.1 Introduction 6.2 Predicate Logics 6.2.1 Syntax and Semantics 6.2.2 Basics of Predicate Logic 6.2.3 Fragments with Decidable Satisfiability Problem 6.2.4 Embedding Modal Logics in Predicate Logic 6.2.5 Predicate Logic on Linearly Ordered Domains 6.3 Monadic Second Order Logic of Linear Order MSO< 6.3.1 Equivalence of S1S and MSO< 6.3.2 Translating MSO< to omega-Automata 6.3.3 B|chi's Decision Procedure: Normal Forms for S1S 6.4 Monadic First Order Logic of Linear Order MFO< 6.5 Non-Monadic Characterizations 7 Conclusions A Binary Decision Diagrams A.1 Basic Definitions A.2 Basic Algorithms on BDDs A.3 Minimization of BDDs Using Care Sets A.4 Computing Successors and Predecessors A.5 Variable Reordering A.6 Final Remarks B Local Model Checking and Satisfiability Checking for the 5-Calculus B.1 A Partial Local Model Checking Procedure B.2 A Complete Local Model Checking Procedure B.3 Satisfiability of 5-Calculus Formulas C Reduction of Structures C.1 Galois Connections and Simulations C.1.1 Basic Properties of Galois Connections C.1.2 Galois Simulation C.2 Abstract Structures and Preservation Results C.3 Optimal and Faithful Abstractions C.4 Data Abstraction C.4.1 Abstract Interpretation of Structures C.4.2 Abstract Specifications C.5 Symmetry and Model Checking C.5.1 Symmetries of Structures C.5.2 Symmetries in the Specification References Index _._________________________________________________________________________._ Conferences _._________________________________________________________________________._ Contributed by: Stephane Lafortune ANNOUNCEMENT AND FIRST CALL FOR PAPERS FOR WODES'06 After an initial DES workshop in Amherst, USA, in 1991, the WODES series of International Workshops on Discrete Event Systems was formally started in 1992. Since then it has been held every other year in Europe. The 8th edition of WODES is coming to the USA in 2006, in Ann Arbor on the campus of the University of Michigan, July 10-12. It will provide researchers from different fields (control theoreticians and control engineers, software engineers and computer scientists, operations research specialists) with an opportunity to exchange information and new ideas, and to discuss new developments in the field of DES theory and application. Authors are invited to submit papers and proposals for special sessions on all aspects of DES research to the workshop secretariat by January 16, 2006. Papers should be submitted electronically in PDF format. Accepted papers will be limited to 6 pages in the proceedings, to be published electronically. Special sessions should consist of 4 to 6 papers along with a 1-2 page description of the aim and content of the session. Papers in special sessions will be reviewed individually. In case the special session is not accepted, individual papers will be considered for inclusion in the regular program. Important Dates January 16, 2006: Submission of papers and special sessions April 17, 2006: Notification of acceptance May 22, 2006: Final versions due July 10-12, 2006: Workshop Organizing Committee and Co-Chairs of Scientific Program Committee Stephane Lafortune (USA) Feng Lin (USA) Dawn Tilbury (USA) Web site http://www.eecs.umich.edu/wodes2006 _._________________________________________________________________________._ Contributed by: Ryan Leduc WORKSHOP ON CONTROL OF HYBRID AND DISCRETE EVENT SYSTEMS Announcing a one-day workshop in Hybrid & Discrete Event Systems to be held in conjunction with the 26th International Conference On Application and Theory of Petri Nets and Other Models of Concurrency (ATPN'05), being held in Miami, Florida, USA, June 20-25, 2005. The workshop will be held on June 21, 2005, and is intended to bring together researchers in the areas of Petri nets and Control of Hybrid and Discrete Event Systems. Specifically, this workshop is intended to present current issues in the area of Hybrid and Discrete Event Systems to the community of Petri net researchers. Petri nets could play an important role in the modeling and computational aspects of supervisory control of Hybrid and Discrete Event Systems. The presentations in the workshop will provide a realistic impression of the state-of-art in the theory of supervisory control of Hybrid and Discrete Event Systems. It is hoped that this workshop will raise fresh and independent theories and tools from the community of Petri net researchers that address several open problems in the area of supervisory control. Last but not least, we hope the workshop will serve as a meeting point for researchers in Petri nets and the control of Hybrid and Discrete Event Systems, which could lead to fruitful collaborations in the future. The main topics that will be covered include: * Modeling and representations * Computability and complexity issues * Tools for analysis and verification * Tools for synthesis and design * Control and optimization * Sciences domains and Engineering applications Organizers: Ramavarapu Sreenivas, (USA) Toshimitsu Ushio, (Japan) Jose-Manuel Colom, (Spain) Web site http://www.cs.fiu.edu/atpn2005/control.php _._________________________________________________________________________._ The End _._________________________________________________________________________._ Mon Mar 28 21:28:45 EST 2005