EPSRC logo

Details of Grant 

EPSRC Reference: EP/H046623/1
Title: Synthesis and Verification in Markov Game Structures
Principal Investigator: Schewe, Professor S
Other Investigators:
Wojtczak, Dr DK Shenton, Dr AT
Researcher Co-Investigators:
Project Partners:
Department: Computer Science
Organisation: University of Liverpool
Scheme: Standard Research
Starts: 01 October 2010 Ends: 30 November 2013 Value (£): 335,487
EPSRC Research Topic Classifications:
Fundamentals of Computing
EPSRC Industrial Sector Classifications:
No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
16 Mar 2010 ICT Prioritisation Panel (March 10) Announced
Summary on Grant Application Form
To meet the objectives of our project, we will divide our research into five work packages.The first work package is devoted to representing the control problems that we want to approach and to identify benchmarks and case studies as guidelines for relevant demands and measures of success for the applied aspects of our project. The starting point for our models will be- a generalisation of interactive Markov chains to 2.5 player games, a model in which the decisions of the different players are physically separated by assigning them to different states, and- a generalisation of Markov decision processes to Markov games, a model in which the decisions of both (or, more generally, of all) players are entangled and represented in the same node.We will extend these models by representations of the observational and computational power of the controllers under consideration, and formalisations of the--simple--objectives we want to meet.Additionally, we will develop benchmarks and case studies to guide the applied aspects of our project, and to root it in different communities--in particular in engineering and IT--by reflecting their respective demands.Work packages two, three, and four from the theoretic core of our work. Our second work package will address the simple question of constructing controllers with complete information, while a third work package will address the generalisation of these techniques to controllers with incomplete information but, for distributed controllers, equivalent information about the system state.Different to discrete systems, the abstraction (or restricted observability) of time plays a paramount role when considering incomplete information of these systems. This particular type of abstraction has proven to often simplify the construction of optimal strategies: The construction of optimal time-abstract strategies (and the proof of their existence) is much simpler than the construction of time dependent ones.The fourth work package refers to the extension of these results to distributed schedulers with different observational power.For work packages two, three, and four, we will study the decidability of quantitative and qualitative safety and reachability properties.In a fifth work package we will focus on algorithmic aspects like the development and selection of appropriate data structures of the model checking and optimisation problems, and develop prototype implementations that solve as a proof-of-concept for their applicability for a selection of the developed approaches. These proof-of-concept implementations will also play an important role in determining the applicability and potential of the techniques developed in the project on the target implementations defined in the first work package, and as means to communicate our results for dissemination and exploitation purposes.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Summary
Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:  
Further Information:  
Organisation Website: http://www.liv.ac.uk