H2020Индивидуална стипендия2020–2022

FouCo · Foundations of Composition

„Хоризонт 2020“ — Действия „Мария Склодовска-Кюри“

Период: 2020-04-01 → 2022-03-31
Финансиране от ЕС: 212 934 €
Участници: 1
Схема: MSCA-IF

Линиите свързват координатора с партньорите.

Накратко на български

Автоматите (формалните приемници) се изследват чрез оптимизиране на техните структури, за да бъдат по-кратки и ефективни при проверка на софтуерни системи. Това помага за създаването на по-надежден хардуер, по-качествен софтуер и подобрени техники в машинното обучение.

Този кратък обзор е генериран от изкуствен интелект

Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.

Резултати накратко

Foundations of Composition

Composition is a key technique in automata theory, used in particular in the model-checking, realisability analysis and automatic synthesis of reactive systems. In plain(ish) English, we develop automata (formal acceptors) that are tailored for these tasks: concise and efficient, doing just what they should, and no more. This pushes the envelope of the doable: more problems are within reach for verifying them, more problems are in reach for learning them with guarantees, etc. This can ultimatively lead to better software, better hardware, and better machine learning techniques in some areas. Thus, while the nature of the project is foundational and we have mainly produced lemmas and theorems, they are on their slow crawl up the technical readiness level and do have the potential to enfold impact.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз

Цел на проекта

Composition is a key technique in automata theory, used in particular in the model-checking, realisability analysis and automatic synthesis of reactive systems. Typically, when it comes to composition, deterministic automata are used as they behave well when composed with other automata or games. However, determinisation is notoriously complex, both conceptually and computationally. One approach to avoiding determinisation is the notion of Good for Games (GFG) nondeterministic automata, which, despite their nondeterminism, compose well with games. Recent work suggests that the notion of GFG automata, so far only used for composing non-deterministic automata with games, is in fact much more powerful: it generalises to alternating automata, a more general and flexible type of automata that is particularly close to formal logics, and such automata can be used not just in composition with games, but with other automata as well. This means that alternating automata of this type could potentially be used in solutions to parity games, Church's synthesis problem, and, more generally, for turning automata into equivalent automata with simpler acceptance conditions.This project aims to study how to make automata compositional, how to recognise compositional automata, and how to exploit compositionality to improve algorithms in verification and synthesis. In particular, we will study how partial notions of composition, that is, automata that are not GFG in general, but can still be composed with a restricted class of games, can be exploited to avoid determinisation and thereby simplify existing algorithms for reactive synthesis, model-checking and Markov decision procedures.

Оригинален текст от CORDIS (на английски).

Участници

THE UNIVERSITY OF LIVERPOOL · LIVERPOOLКоординаторОбединеното кралство