arXiv subjects

Andreas Morgenstern

Publications and source records attributed to Andreas Morgenstern.

3 recordsLinked to original sources

arXiv2021

From Complexity Measurement to Holistic Quality Evaluation for Automotive Software Development

In recent years, the role and the importance of software in the automotive domain have changed dramatically. Being able to systematically evaluate and manage software quality is becoming even more crucial. In practice, however, we still find a largely static approach for measuring software quality based on a predefined list of complexity metrics with static thresholds to fulfill. We propose using a more flexible framework instead, which systematically derives measures and evaluation rules based on the goals and context of a development project.

cs.SE↗

arXiv2011

A LTL Fragment for GR(1)-Synthesis

The idea of automatic synthesis of reactive programs starting from temporal logic (LTL) specifications is quite old, but was commonly thought to be infeasible due to the known double exponential complexity of the problem. However, new ideas have recently renewed the interest in LTL synthesis: One major new contribution in this area is the recent work of Piterman et al. who showed how polynomial time synthesis can be achieved for a large class of LTL specifications that is expressive enough to cover many practical examples. These LTL specifications are equivalent to omega-automata having a so-called GR(1) acceptance condition. This approach has been used to automatically synthesize implementations of real-world applications. To this end, manually written deterministic omega-automata having GR(1) conditions were used instead of the original LTL specifications. However, manually generating deterministic monitors is, of course, a hard and error-prone task. In this paper, we therefore present algorithms to automatically translate specifications of a remarkable large fragment of LTL to deterministic monitors having a GR(1) acceptance condition so that the synthesis algorithms can start with more readable LTL specifications.

cs.LO↗

arXiv2010

Exploiting the Temporal Logic Hierarchy and the Non-Confluence Property for Efficient LTL Synthesis

The classic approaches to synthesize a reactive system from a linear temporal logic (LTL) specification first translate the given LTL formula to an equivalent omega-automaton and then compute a winning strategy for the corresponding omega-regular game. To this end, the obtained omega-automata have to be (pseudo)-determinized where typically a variant of Safra's determinization procedure is used. In this paper, we show that this determinization step can be significantly improved for tool implementations by replacing Safra's determinization by simpler determinization procedures. In particular, we exploit (1) the temporal logic hierarchy that corresponds to the well-known automata hierarchy consisting of safety, liveness, Buechi, and co-Buechi automata as well as their boolean closures, (2) the non-confluence property of omega-automata that result from certain translations of LTL formulas, and (3) symbolic implementations of determinization procedures for the Rabin-Scott and the Miyano-Hayashi breakpoint construction. In particular, we present convincing experimental results that demonstrate the practical applicability of our new synthesis procedure.

cs.LO↗