Project Work of T-79.5301 Reactive Systems, Spring 2006 A Competition for Checking Emptiness of Büchi automata An automata theoretic approach to model check LTL formulas is based on (i) constructing an automaton that represents a negation of the correctness property, and (ii) checking that the language recognised by the product Büchi automaton of the system and the property automaton is empty. Therefore, checking the emptiness of Büchi automata is a crucial task in verification. The project work is to implement an emptiness checker for Büchi automata and participate in emptiness checker competition as described below. You may freely choose algorithms, data structures etc. as long as the following requirements will be satisfied. Entrants An entrant to the emptiness checker competition is your implementation of an emptiness checker for Büchi automata submitted in source code format by way of email to the lecturer. The submission deadline is April 9. Each submission must include a README file explaining how to compile and install the checker. In addition, each submission must include a brief (1-2 pages) description of the checker. This should describe the algorithms and data structures that are used in the checker. Input and output formats The emptiness checker must read a Büchi automaton instance from a file given as a parameter, e.g., ./checker instance If a checker uses random numbers, it must accept a second seed parameter, where seed is a number, e.g., ./checker instance 123 The automaton will be represented by a directed graph whose k nodes are 0,1,...,k-1 and where 0 represents the initial state of the automaton. The transition labels will be omitted. The used input format is very simple, each line contains (separated by spaces): - state of automaton - either 1 or 0 depending whether or not the state is accepting - sequence of nodes representing the successor states Consequently, the input file for an automaton with k states should contain k lines. The checker should display messages on the standard output that will be used to check the results. The output format is the following. The solution should be displayed in one line. This line must only contain one char " c " which must be either e (automaton is empty) or n (automaton is nonempty). Execution Environment During the competition all emptiness checkers will run on a machine with the following specifications: - Operating System: Debian Linux, kernel version 2.4.26-1 - Processor: AMD Athlon, 1.0 GHz - Memory: 1 GB - Compilers: gcc version 3.3.5, javac 1.5.0_05 Benchmark Selection The benchmarks for the competition will be selected out of a set of randomly generated automata instances. Competition The competition will take place shortly after the submission deadline. Each checker will have to process 100 automata instances. For each checker and instance, a run-time limit of 5 minutes will be imposed. Assessment of Emptiness Checkers Checkers will be evaluated based on a score that takes into account: - the number of instances solved within the run-time limit, and - the total time needed to solve all instances. The results of the performance comparison will be discussed and the winner will be announced before the last lecture. Qualification Round Before the actual competition there will be a qualification round in order to validate the emptiness checkers. In order to pass there should be neither wrong results on simple test automata nor deviation from input/output format requirements. You will get your final grade (pass/fail) based on the qualification round. Reading List The following publications may be useful: - Chapter 9 of E.M. Clarke, O. Grumberg, and D.A. Peled: Model Checking, MIT Press 1999. - C. Courcoubetis, M.Y. Vardi, P. Wolper, and M. Yannakakis: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design 1(2/3), pp. 275-288, 1992. - J. Geldenhuys and A. Valmari: More Efficient On-the-fly LTL Verification with Tarjan's Algorithm. Theoretical Computer Science Vol. 345 1, pp. 60-82, 2005.