NDLI: Measuring and Synthesizing Systems in Probabilistic Environments

Content Provider	ACM Digital Library
Author	Chatterjee, Krishnendu Henzinger, Thomas A. Jobstmann, Barbara Singh, Rohit
Copyright Year	2015
Abstract	The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value. For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter, for all ε > 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.
Starting Page	1
Ending Page	34
Page Count	34
File Format	PDF
ISSN	00045411
e-ISSN	1557735X
DOI	10.1145/2699430
Journal	Journal of the ACM (JACM)
Volume Number	62
Issue Number	1
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2015-03-02
Publisher Place	New York
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Synthesis Quantitative verification
Content Type	Text
Resource Type	Article
Subject	Hardware and Architecture Information Systems Control and Systems Engineering Artificial Intelligence Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Fast Probabilistic Algorithms for Verification of Polynomial Identities

Complexity of Synthesizing Inductive Assertions

Probabilistic inductive inference

Path Calculus in Program Verification

Aggregate operators in probabilistic databases

Relativized Questions Involving Probabilistic Algorithms

On Relevance, Probabilistic Indexing and Information Retrieval

Verification Decidability of Presburger Array Programs

The complexity of probabilistic verification

Measuring and Synthesizing Systems in Probabilistic Environments

Similar Documents

Fast Probabilistic Algorithms for Verification of Polynomial Identities

Complexity of Synthesizing Inductive Assertions

Probabilistic inductive inference

Path Calculus in Program Verification

Aggregate operators in probabilistic databases

Relativized Questions Involving Probabilistic Algorithms

On Relevance, Probabilistic Indexing and Information Retrieval

Verification Decidability of Presburger Array Programs

The complexity of probabilistic verification

Measuring and Synthesizing Systems in Probabilistic Environments