@inproceedings{4373, author = {Maler, Oded and Dejan Nickovic and Pnueli,Amir}, pages = {2 -- 16}, publisher = {Springer}, title = {{Real Time Temporal Logic: Past, Present, Future}}, doi = {1571}, year = {2006}, } @inproceedings{4374, author = {Maler, Oded and Dejan Nickovic and Pnueli,Amir}, pages = {274 -- 289}, publisher = {Springer}, title = {{From MITL to Timed Automata}}, doi = {1570}, year = {2006}, } @inproceedings{4406, abstract = {We propose and evaluate a new algorithm for checking the universality of nondeterministic finite automata. In contrast to the standard algorithm, which uses the subset construction to explicitly determinize the automaton, we keep the determinization step implicit. Our algorithm computes the least fixed point of a monotone function on the lattice of antichains of state sets. We evaluate the performance of our algorithm experimentally using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, the antichain algorithm outperforms the standard one by several orders of magnitude. We also show how variations of the antichain method can be used for solving the language-inclusion problem for nondeterministic finite automata, and the emptiness problem for alternating finite automata.}, author = {De Wulf, Martin and Doyen, Laurent and Thomas Henzinger and Raskin, Jean-François}, pages = {17 -- 30}, publisher = {Springer}, title = {{Antichains: A new algorithm for checking universality of finite automata}}, doi = {10.1007/11817963_5}, volume = {4144}, year = {2006}, } @inproceedings{4401, author = {Alur, Rajeev and Pavol Cerny and Zdancewic,Steve}, pages = {107 -- 118}, publisher = {Springer}, title = {{Preserving Secrecy Under Refinement}}, doi = {1543}, year = {2006}, } @inproceedings{4437, abstract = {The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.}, author = {Thomas Henzinger and Piterman, Nir}, pages = {395 -- 410}, publisher = {Springer}, title = {{Solving games without determinization}}, doi = {10.1007/11874683_26}, volume = {4207}, year = {2006}, }