Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userTypestates to Automata and back: a tool
57
0
0.0
(
0
)
Added by
EPTCS
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Development of software is an iterative process. Graphical tools to represent the relevant entities and processes can be helpful. In particular, automata capture well the intended execution flow of applications, and are thus behind many formal approaches, namely behavioral types. Typestate-oriented programming allow us to model and validate the intended protocol of applications, not only providing a top-down approach to the development of software, but also coping well with compositional development. Moreover, it provides important static guarantees like protocol fidelity and some forms of progress. Mungo is a front-end tool for Java that associates a typestate describing the valid orders of method calls to each class, and statically checks that the code of all classes follows the prescribed order of method calls. To assist programming with Mungo, as typestates are textual descriptions that are terms of an elaborate grammar, we developed a tool that bidirectionally converts typestates into an adequate form of automata, providing on one direction a visualization of the underlying protocol specified by the typestate, and on the reverse direction a way to get a syntactically correct typestate from the more intuitive automata representation.
rate research
Read More
We present TarTar, an automatic repair analysis tool that, given a timed diagnostic trace (TDT) obtained during the model checking of a timed automaton model, suggests possible syntactic repairs of the analyzed model. The suggested repairs include modified values for clock bounds in location invariants and transition guards, adding or removing clock resets, etc. The proposed repairs are guaranteed to eliminate executability of the given TDT, while preserving the overall functional behavior of the system. We give insights into the design and architecture of TarTar, and show that it can successfully repair 69% of the seeded errors in system models taken from a diverse suite of case studies.
Controller synthesis for general linear temporal logic (LTL) objectives is a challenging task. The standard approach involves translating the LTL objective into a deterministic parity automaton (DPA) by means of the Safra-Piterman construction. One of the challenges is the size of the DPA, which often grows very fast in practice, and can reach double exponential size in the length of the LTL formula. In this paper we describe a single exponential translation from limit-deterministic Buchi automata (LDBA) to DPA, and show that it can be concatenated with a recent efficient translation from LTL to LDBA to yield a double exponential, enquote{Safraless} LTL-to-DPA construction. We also report on an implementation, a comparison with the SPOT library, and performance on several sets of formulas, including instances from the 2016 SyntComp competition.
Equality and disjointness are two of the most studied problems in communication complexity. They have been studied for both classical and also quantum communication and for various models and modes of communication. Buhrman et al. [Buh98] proved that the exact quantum communication complexity for a promise version of the equality problem is ${bf O}(log {n})$ while the classical deterministic communication complexity is $n+1$ for two-way communication, which was the first impressively large (exponential) gap between quantum and classical (deterministic and probabilistic) communication complexity. If an error is tolerated, both quantum and probabilistic communication complexities for equality are ${bf O}(log {n})$. However, even if an error is tolerated, the gaps between quantum (probabilistic) and deterministic complexity are not larger than quadratic for the disjointness problem. It is therefore interesting to ask whether there are some promis
We introduce a way to parameterize automata and games on finite graphs with natural numbers. The parameters are accessed essentially by allowing counting down from the parameter value to 0 and branching depending on whether 0 has been reached. The main technical result is that in games, a player can win for some values of the parameters at all, if she can win for some values below an exponential bound. For many winning conditions, this implies decidability of any statements about a player being able to win with arbitrary quantification over the parameter values. While the result seems broadly applicable, a specific motivation comes from the study of chains of strategies in games. Chains of games were recently suggested as a means to define a rationality notion based on dominance that works well with quantitative games by Bassett, Jecker, P., Raskin and Van den Boogard. From the main result of this paper, we obtain generalizations of their decidability results with much simpler proofs. As both a core technical notion in the proof of the main result, and as a notion of potential independent interest, we look at boolean functions defined via graph game forms. Graph game forms have properties akin to monotone circuits, albeit are more concise. We raise some open questions regarding how concise they are exactly, which have a flavour similar to circuit complexity. Answers to these questions could improve the bounds in the main theorem.
The Behavior-Interaction-Priority (BIP) framework, rooted in rigorous semantics, allows the construction of systems that are correct-by-design. BIP has been effectively used for the construction and analysis of large systems such as robot controllers and satellite on-board software. Nevertheless, the specification of BIP models is done in a purely textual manner without any code editor support. To facilitate the specification of BIP models, we present DesignBIP, a web-based, collaborative, version-controlled design studio. To promote model scaling and reusability of BIP models, we use a graphical language for modeling parameterized BIP models with rigorous semantics. We present the various services provided by the design studio, including model editors, code editors, consistency checking mechanisms, code generators, and integration with the JavaBIP tool-set.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
