The Complexity of Synthesis from Probabilistic Components

DOI10.1007/978-3-662-47666-6_9MaRDI QIDQ3449469zbMATH OpenOpenAlexFDO

Authors Krishnendu Chatterjee, Laurent Doyen, Moshe Y. Vardi

Publication date 4 November 2015

Published in Automata, Languages, and Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1502.04844

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: The synthesis problem asks for the automatic construction of a system from its specification. In the traditional setting, the system is "constructed from scratch" rather than composed from reusable components. However, this is rare in practice, and almost every non-trivial software system relies heavily on the use of libraries of reusable components. Recently, Lustig and Vardi introduced dataflow and controlflow synthesis from libraries of reusable components. They proved that dataflow synthesis is undecidable, while controlflow synthesis is decidable. The problem of controlflow synthesis from libraries of probabilistic components was considered by Nain, Lustig and Vardi, and was shown to be decidable for qualitative analysis (that asks that the specification be satisfied with probability 1). Our main contributions for controlflow synthesis from probabilistic components are to establish better complexity bounds for the qualitative analysis problem, and to show that the more general quantitative problem is undecidable. For the qualitative analysis, we show that the problem (i) is EXPTIME-complete when the specification is given as a deterministic parity word automaton, improving the previously known 2EXPTIME upper bound; and (ii) belongs to UP $cap$ coUP and is parity-games hard, when the specification is given directly as a parity condition on the components, improving the previously known EXPTIME upper bound.

Recommendations

• Synthesis from probabilistic components
• Synthesis from probabilistic components
• scientific article; zbMATH DE number 1863173
• Synthesis for Probabilistic Environments
• Synthesizing efficient systems in probabilistic environments
• FM 2005: Formal Methods
• The complexity of rational synthesis
• Compositionality of approximate bisimulation for probabilistic systems
• Compositional abstraction techniques for probabilistic automata

Cites work

• scientific article; zbMATH DE number 4124989 (Why is no real title available?)
• scientific article; zbMATH DE number 2080757 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• scientific article; zbMATH DE number 3371972 (Why is no real title available?)
• Modular synthesis with open components
• Quantitative stochastic parity games
• Reduction of stochastic parity to stochastic mean-payoff games
• Synthesis from Component Libraries
• Synthesis from component libraries with costs
• Synthesis from probabilistic components
• The Complexity of Synthesis from Probabilistic Components
• The complexity of partial-observation stochastic parity games with finite-memory strategies
• The complexity of probabilistic verification
• The complexity of solving stochastic games on graphs

Cited in

(10)

• Synthesis from component libraries with costs
• A general modular synthesis problem for pushdown systems
• Modular synthesis with open components
• Synthesis from recursive-components libraries
• The Complexity of Synthesis from Probabilistic Components
• Synthesis from Component Libraries
• On the hardness of priority synthesis
• Synthesis from probabilistic components
• Synthesis from probabilistic components
• Synthesizing Probabilistic Invariants via Doob’s Decomposition

Describes a project that uses

Uses Software

• PRISM

This page was built for publication: The Complexity of Synthesis from Probabilistic Components

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3449469)