Search

The determinization of Buchi automata is a celebrated problem, with applications in synthesis, probabilistic verification, and multi-agent systems. Since the 1960s, there has been a steady progress of constructions: by McNaughton, Safra, Piterman, Schewe, and others. Despite the proliferation of solutions, they are all essentially ad-hoc constructions, with little theory behind them other than proofs of correctness. Since Safra, all optimal constructions employ trees as states of the deterministic automaton, and transitions between states are defined operationally over these trees. The operational nature of these constructions complicates understanding, implementing, and reasoning about them, and should be contrasted with complementation, where a solid theory in terms of automata run DAGs underlies modern constructions. In 2010, we described a profile-based approach to Buchi complementation, where a profile is simply the history of visits to accepting states. We developed a structural theory of profiles and used it to describe a complementation construction that is deterministic in the limit. Here we extend the theory of profiles to prove that every run DAG contains a profile tree with at most a finite number of infinite branches. We then show that this property provides a theoretical grounding for a new determinization construction where macrostates are doubly preordered sets of states. In contrast to extant determinization constructions, transitions in the new construction are described declaratively rather than operationally., Comment: In Proceedings GandALF 2013, arXiv:1307.4162

Dynamical systems are used to model a variety of time-dependent systems. Visualizations of dynamical systems can display a large amount of information in a single image, but generating these images requires both mathematical and programming expertise. dsmodels is a domain-specific language (DSL) for visualizing two-dimensional dynamical systems. dsmodels speeds up the process of visualizing a dynamical system by providing primitives to capture models, encapsulate features, and depict the overall behavior of the system. dsmodels can also simulate dynamical systems to compute attractors and their basis of attraction, allowing for rapid prototyping or informal analysis. We present dsmodels using a case study of population models.

Automata-theoretic formal verification approaches the problem of guaranteeing that a program conforms to its specification by reducing conformance to language containment. We can prove conformance by representing both programs and specifications as automata and proving that the specification contains the program. This connection to the theory of automata on infinite words motivated an extensive research program into the algorithmic theory of automata on infinite words, with a focus on algorithms that perform well in practice. The focus on practical performance is important because of the large gap between worst-case complexity and practice for many automata-theoretic algorithms. Unfortunately, there are few benchmark instances of automata in industrial verification. To overcome this challenge, Tabakov and Vardi proposed a model for generating random automata as test cases. The Tabakov-Vardi T-V model, however, is just one random model, based on a specific, rather simple model of random graphs. Other models of random graphs have been studied over the years. While the T-V model has the advantage of simplicity, it is not clear that performance analysis conducted on this model is robust, and an analogous analysis over other random models might yield different conclusions. To address this problem, we introduce three novel models of random automata, yielding automata that are richer in structure than the automata generated by the T-V model. By generating large corpora of random automata and using them to evaluate the performance of universality-checking algorithms, we show that the T-V model is a robust random model for evaluating performance of universality-checking algorithms.

Students designed and built lights for global students who did not have access to reliable clean light and as a result, could not study after sunset. UNESCO estimates 1.5B people worldwide do not have access to clean light and that has major negative ramifications towards the Millennial Goals for Education. School could be used to educate not only the students who are receiving lights, but also the students who are engineering the lights. Primary, middle and high school students from Colorado, Canada and the UK, collaborated in the designing process and produced different light designs to solve real problems for real people. The Colorado Lantern was a 3D printed plug-in rechargeable light designed by Preston Middle School. The Riverview High School Podium and Clam lights were 3D printed table top solar rechargeable lights. The Pheasey Park Elementary and RHS collaboration yielded a few versions of a wearable light. Engineering Brightness, Philanthropic Engineering's (http://p-e.io) flagship project, aims to deliberately engineer brightness on many different fronts including: • in the rooms of studying students all over the world who otherwise do not have access to clean light. • in the minds of students who bring many skills and aptitudes to bear in the design and production of lights. • in the hearts of students who use their learning to impact the lives of others. The project provided novel motivation for studying. If the work was mediocre, it was much more devastating than a poor mark, as someone else's life was negatively impacted. The work superseded a grade and survived being thrown out at the end of the semester. We are proud to be leaving a legacy, and plan to keep participating, even after we move on to another school. Our work has been featured in a documentary, numerous television news articles, the front page of NSTA and we have been asked to present at WeDay-Alberta. As students, we would like to present the design evolution, our current prototypes, the impact we are making in nine countries and our future plans to recruit more schools to help engineer brightness around the world.

Complementation of B\"uchi automata, required for checking automata containment, is of major theoretical and practical interest in formal verification. We consider two recent approaches to complementation. The first is the rank-based approach of Kupferman and Vardi, which operates over a DAG that embodies all runs of the automaton. This approach is based on the observation that the vertices of this DAG can be ranked in a certain way, termed an odd ranking, iff all runs are rejecting. The second is the slice-based approach of K\"ahler and Wilke. This approach tracks levels of "split trees" - run trees in which only essential information about the history of each run is maintained. While the slice-based construction is conceptually simple, the complementing automata it generates are exponentially larger than those of the recent rank-based construction of Schewe, and it suffers from the difficulty of symbolically encoding levels of split trees. In this work we reformulate the slice-based approach in terms of run DAGs and preorders over states. In doing so, we begin to draw parallels between the rank-based and slice-based approaches. Through deeper analysis of the slice-based approach, we strongly restrict the nondeterminism it generates. We are then able to employ the slice-based approach to provide a new odd ranking, called a retrospective ranking, that is different from the one provided by Kupferman and Vardi. This new ranking allows us to construct a deterministic-in-the-limit rank-based automaton with a highly restricted transition function. Further, by phrasing the slice-based approach in terms of ranks, our approach affords a simple symbolic encoding and achieves the tight bound of Schewe's construction

We compare tools for complementing nondeterministic B\"uchi automata with a recent termination-analysis algorithm. Complementation of B\"uchi automata is a key step in program verification. Early constructions using a Ramsey-based argument have been supplanted by rank-based constructions with exponentially better bounds. In 2001 Lee et al. presented the size-change termination (SCT) problem, along with both a reduction to B\"uchi automata and a Ramsey-based algorithm. The Ramsey-based algorithm was presented as a more practical alternative to the automata-theoretic approach, but strongly resembles the initial complementation constructions for B\"uchi automata. We prove that the SCT algorithm is a specialized realization of the Ramsey-based complementation construction. To do so, we extend the Ramsey-based complementation construction to provide a containment-testing algorithm. Surprisingly, empirical analysis suggests that despite the massive gap in worst-case complexity, Ramsey-based approaches are superior over the domain of SCT problems. Upon further analysis we discover an interesting property of the problem space that both explains this result and provides a chance to improve rank-based tools. With these improvements, we show that theoretical gains in efficiency of the rank-based approach are mirrored in empirical performance.

Buchi complementation has been studied for five decades since the formalism was introduced in 1960. Known complementation constructions can be classified into Ramsey-based, determinization-based, rank-based, and slice-based approaches. For the performance of these approaches, there have been several complexity analyses but very few experimental results. What especially lacks is a comparative experiment on all the four approaches to see how they perform in practice. In this paper, we review the state of Buchi complementation, propose several optimization heuristics, and perform comparative experimentation on the four approaches. The experimental results show that the determinizationbased Safra-Piterman construction outperforms the other three and our heuristics substantially improve the Safra-Piterman construction and the slice-based construction.

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate Fω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.