Mostra i principali dati dell'item

dc.contributor.authorDe Crescenzo, Ilaria
dc.date.accessioned2017-03-01T11:26:02Z
dc.date.available2017-03-01T11:26:02Z
dc.date.issued2016-05-18
dc.identifier.urihttp://hdl.handle.net/10556/2334
dc.identifier.urihttp://dx.doi.org/10.14273/unisa-749
dc.description2013 - 2014it_IT
dc.description.abstractThis thesis is focused on synthesis. In formal veri cation synthesis can be referred to the controller synthesis and the system synthesis. This work combines both this area of research. First we focus on synthesizing modular controllers considering game on recursive game graph with the requirement that the strategy for the protagonist must be modular. A recursive game graph is composed of a set of modules, whose vertices can be standard vertices or can correspond to invocations of other modules and the standard and the set of vertices is split into two sets each controlled by one of the players. A strategy is modular if it is local to a module and is oblivious to previous module invocations, and thus does not depend on the context of invocation. We study for the rst time modular strategies with respect to winning conditions that can be expressed languages of pushdown automata. We show that pushdown modular games are undecidable in general, and become decidable for visibly pushdown automata speci cations. We carefully characterize the computational complexity of the considered decision problem. In particular, we show that modular games with a universal B uchi or co-B uchi visibly pushdown winning condition are Exptime-complete, and when the winning condition is given as a CaRet or Nwtl temporal logic formula the problem is 2Exptime-complete, and it remains 2Exptime-hard even for simple fragments of these logics. As a further contribution, we present a di erent synthesis algorithm that runs faster than known solutions for large speci cations and many exits. In the second part of this thesis, we introduce and solve a new componentbased synthesis problem that subsumes the synthesis from libraries of recursive components introduced by Lustig and Vardi with the modular synthesis introduced by Alur et al. for recursive game graphs. We model the components of our libraries as game modules of a recursive game graph with unmapped boxes, and consider as correctness speci cation a target set of vertices. To solve this problem, we give an exponential-time xed-point algorithm that computes annotations for the vertices of the library components by exploring them backwards. We show a matching lower-bound via a direct reduction from linear-space alternating Turing machines, thus proving Exptime-completeness. We also give a second algorithm that solves this problem by annotating in a table the result of many local reachability game queries on each game component. This algorithm is exponential only in the number of the exits of the game components, and thus shows that the problem is xed-parameter tractable. Finally, we study a more general synthesis problem for component-based pushdown systems, the modular synthesis from a library of components (Lms). We model each component as a game graph with boxes as placeholders for calls to components, as in the previous model, but now the library is equipped also with a box-to-component map that is a partial function from boxes to components. An instance of a component C is essentially a copy of C along with a local strategy that resolves the nondeterminism of pl 0. An RSM S synthesized from a library is a set of instances along with a total function that maps each box in S to an instance of S and is consistent with the box-to-component map of the library. We give a solution to the Lms problem with winning conditions given as internal reachability objectives, or as external deterministic nite automata (FA) and deterministic visibly pushdown automata (VPA) (6). We show that the Lms problem is Exptime-complete for any of the considered speci cations. [edited by Author]it_IT
dc.language.isoenit_IT
dc.publisherUniversita degli studi di Salernoit_IT
dc.subjectSynthesisit_IT
dc.subjectLibraryit_IT
dc.subjectModularit_IT
dc.titleSynthesis of recursive state machines from libraries of game modulesit_IT
dc.typeDoctoral Thesisit_IT
dc.subject.miurINF/01 INFORMATICAit_IT
dc.contributor.coordinatorePersiano, Giuseppeit_IT
dc.description.cicloXIII n.s.it_IT
dc.contributor.tutorLa Torre, Salvatoreit_IT
dc.identifier.DipartimentoScienze Matematiche, Fisiche e Naturaliit_IT
 Find Full text

Files in questo item

Thumbnail
Thumbnail

Questo item appare nelle seguenti collezioni

Mostra i principali dati dell'item