Zobrazeno 1 - 10
of 99
pro vyhledávání: '"Maoz, Shahar"'
Autor:
Maoz, Shahar, Shalom, Rafi
One of the main challenges of reactive synthesis, an automated procedure to obtain a correct-by-construction reactive system, is to deal with unrealizable specifications. One means to deal with unrealizability, in the context of GR(1), an expressive
Externí odkaz:
http://arxiv.org/abs/2103.00297
$\omega$-regular energy games, which are weighted two-player turn-based games with the quantitative objective to keep the energy levels non-negative, have been used in the context of verification and synthesis. The logic of modal $\mu$-calculus, when
Externí odkaz:
http://arxiv.org/abs/2005.00641
Autor:
Maoz, Shahar, Ringert, Jan Oliver
Spectra is a new specification language for reactive systems, specifically tailored for the context of reactive synthesis. The meaning of Spectra is defined by a translation to a kernel language. Spectra comes with the Spectra Tools, a set of analyse
Externí odkaz:
http://arxiv.org/abs/1904.06668
Publikováno v:
EPTCS 260, 2017, pp. 62-80
Reactive synthesis for the GR(1) fragment of LTL has been implemented and studied in many works. In this workshop paper we present and evaluate a list of heuristics to potentially reduce running times for GR(1) synthesis and related algorithms. The l
Externí odkaz:
http://arxiv.org/abs/1712.01103
Publikováno v:
EPTCS 229, 2016, pp. 35-54
Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one
Externí odkaz:
http://arxiv.org/abs/1611.07622
Autor:
Maoz, Shahar, Ringert, Jan Oliver
Publikováno v:
EPTCS 202, 2016, pp. 58-72
Reactive synthesis is an automated procedure to obtain a correct-by-construction reactive system from a given specification. GR(1) is a well-known fragment of linear temporal logic (LTL) where synthesis is possible using a polynomial symbolic algorit
Externí odkaz:
http://arxiv.org/abs/1602.01172
Publikováno v:
Proceedings Int. Workshop on Models and Evolution (ME'10), co-located with MoDELS'10. J. Dingel and A. Solberg (Eds.): MoDELS Workshops, LNCS 6627, pp. 194 - 203, 2010
Models are heavily used in software engineering and together with their systems they evolve over time. Thus, managing their changes is an important challenge for system maintainability. Existing approaches to model differencing concentrate on heurist
Externí odkaz:
http://arxiv.org/abs/1409.2485
This document defines an operational semantics for activity diagrams (ADs) using a translation to SMV. The translation is inspired by the work of Eshuis [Esh06] and extends it with support for data. Each execution step of the SMV module obtained from
Externí odkaz:
http://arxiv.org/abs/1409.2356
Publikováno v:
Proc. 25th Euro. Conf. on Object Oriented Programming (ECOOP'11), LNCS 6813, pp. 281-305, Springer, 2011
While object diagrams (ODs) are widely used as a means to document object-oriented systems, they are expressively weak, as they are limited to describe specific possible snapshots of the system at hand. In this paper we introduce modal object diagram
Externí odkaz:
http://arxiv.org/abs/1409.2353
Publikováno v:
Proc. 25th Euro. Conf. on Object Oriented Programming (ECOOP'11), LNCS 6813, pp. 230-254, Springer, 2011
Class diagrams (CDs), which specify classes and the relationships between them, are widely used for modeling the structure of object-oriented systems. As models, programs, and systems evolve over time, during the development lifecycle and beyond it,
Externí odkaz:
http://arxiv.org/abs/1409.2355