Synthesis and Verification in Markov Game Structures

Lead Research Organisation: University of Liverpool
Department Name: Computer Science

Abstract

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.

Planned Impact

The long term aim of our research is to develop feasible techniques for the automatic development of high quality control strategies. We consider this research effort to be an important step towards this goal: The expected results will provide us with a thorough understanding of the theoretical as well as of the practical challenges involved in the construction and approximation of optimal control. During the conduct of the research effort, we expect to gain insights and experience in the automated design of good scheduling policies that will lead to efficient algorithmic solutions and proof-of-concept implementations to prove their feasibility. These results can serve as a foundation for follow-up research that can lead to - the construction of first and second generation tools that tap the potential of the developed algorithmic concepts; - an extension of the conceptual coverage of research questions, for example by including cost functions or by integrating a symbolic representation of data; and - the integration of technical restrictions of industrial controllers. After completion of the project, we expect our results to gradually mature from an academic proofs-of-concept to wider applicability in these directions. Starting with the development of efficient tools for the automated analysis of the specifications in the languages developed during this research effort, we envisage the development of tools with gradually increasing expressive power and efficiency, guided by the demands of the engineering and IT industry and scientific curiosity alike. It is our belief that such tools could quickly become powerful enough to attack small applications of industrial interest, and finally extend to applicability in the development of complex control scenarios, whose analysis defies traditional manual approaches. Our results will therefore benefit the regional and national engineering industry on the long run, because our results will lead to improved control strategies, and hence to higher time and energy efficiency. The general public will benefit from this through reduced costs.

Publications

10 25 50

publication icon
Bloem R (2017) CTL* synthesis via LTL synthesis in Electronic Proceedings in Theoretical Computer Science

publication icon
Ernst Moritz Hahn (Co-Author) (2014) IscasMC: A Web-Based Probabilistic Model Checker

publication icon
Fearnley J (2013) Time and Parallelizability Results for Parity Games with Bounded Tree and DAG Width in Logical Methods in Computer Science

publication icon
Fearnley J (2016) Efficient approximation of optimal control for continuous-time Markov games in Information and Computation

publication icon
Fearnley J (2019) An ordered approach to solving parity games in quasi-polynomial time and quasi-linear space in International Journal on Software Tools for Technology Transfer

publication icon
Fearnley J (2012) Algorithmic Game Theory

 
Description We have developed

1. techniques for finding small and concise solutions to optimisation and verification problems,

2. techniques for the fast approximation of optimal solutions for Markov games and decision processes,

3. techniques that capitalise on the scarceness of faults without referring to probabilities, and

4. specialised solutions for related games with special structures.



We have also established the existence of finite optimal control for Markov games and decision processes, of optimal (albeit not finite) control for Markov games played on timed automata, and the non-existence of optimal control for Markov games with one player without access to time.
Exploitation Route The route of making the probabilities abstract in an approach that optimises the fast recovery from rather than the number of tolerable faults is a very simple approach with the potential of being applied. The techniques for finding small and succinct models has potential, but currently lacks a good guidance for finding the solutions. The ad-hoc solutions use SAT and SMT solvers, but it seems that their search heuristics are inappropriate for the problem class. Genetic algorithms have been used with slightly better success, but there are more techniques -- like learning based ones -- that have not been tried yet.



A more immediate route to exploitation is given through the development of an efficient and easy-to-use model checker, IscasMC. This web-based model checker facilitates automata based techniques developed in this project and will be a platform for follow-up work.
Sectors Digital/Communication/Information Technologies (including Software)

 
Description Analysis of Probabilistic Systems
Amount £11,950 (GBP)
Organisation The Leverhulme Trust 
Sector Charity/Non Profit
Country United Kingdom
Start 11/2011 
End 07/2012
 
Description Liverpool India Fellowships
Amount £8,200 (GBP)
Organisation University of Liverpool 
Sector Academic/University
Country United Kingdom
Start 05/2014 
End 10/2014
 
Description Visiting Fellowship
Amount £3,000 (GBP)
Organisation University of Liverpool 
Sector Academic/University
Country United Kingdom
Start 04/2014 
End 05/2014