Details of Grant 

EPSRC Reference:	EP/E022030/1
Title:	Games for Quantitative Analysis of Real Time Systems
Principal Investigator:	Jurdzinski, Dr M
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of Warwick
Scheme:	First Grant Scheme
Starts:	01 September 2007	Ends:	31 August 2010	Value (£):	118,458
EPSRC Research Topic Classifications:	Fundamentals of Computing Logic & Combinatorics
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Algorithmic formal methods are a collection of mathematical models andalgorithmic techniques for computer aided systems engineering. Bysystems engineering we mean modelling, design, quality control,performance evaluation, optimal control, etc., of modern complex computational systems. Examples of such systems include hardware and(embedded) software, but also industrial processes, e-commerceservices, biochemical regulatory networks. Temporal logic modelchecking is one of the recent success stories of theoretical computerscience. Amir Pnueli won the Turing Award in 1996 for introducingtemporal logic into computer science, and the 2000 Goedel Prize andthe 1998 and 2005 ACM Kanellakis Theory and Practice Awards were givento researchers in the community for the development of symbolic andautomata theoretic model checking.Formal methods valuably complement traditional approaches to qualitycontrol in systems engineering such as simulation and testing.The industrial acceptance of model checking techniques is due to theirextra benefits. One of them is the automation of formal analysisachieved by focus on developing efficient algorithms. Another benefitis informative feedback provided to the designer when faults are detected.The applicability of formal methods in systems engineering depends onautomation of analysis methods as well as on having appropriatemathematical models of the analyzed systems and their desiredproperties. The classical model checking methods apply to verificationof non-terminating and discrete time reactive systems modeled usingfinite automata. Modern complex embedded systems are built out of manyheterogenous components that interact with a (possibly adversarial)physical environment. In order to faithfully model such systems thefollowing extensions to the basic automata models andanalysis tasks are considered. Models can be: deterministic orstochastic; and discrete time or real time. The analysis can be:qualitative (deciding yes/no properties) or quantitative (optimizationof performance measures); and performed through verification(non-adversarial) or synthesis (adversarial).The mathematical roots of the automata theoretic model checkingtechniques can be traced to the powerful decidability results forlogics and finite automata on infinite words and trees. The study of(stochastic) real time models with adversarial interaction andquantitative performance measures calls for concepts developed within(stochastic) game theory and control theory. As traditional modelchecking is about qualitative verification (given a system and aqualitative property, determine whether the system satisfies theproperty or not), the analysis of the richer models we argue for isabout (stochastic) quantitative real time synthesis (given aquantitative objective, synthesize a real time strategy/controller forthe system that optimizes the objective). The algorithmic techniquesfor qualitative and quantitative synthesis, for quantitative real timeverification, and for qualitative real time verification andsynthesis, have attracted a lot of attention, but algorithmic resultsfor quantitative real time synthesis are very recent and incomplete.Timed automata are real time models which enjoy efficient algorithmicmethods for qualitative and quantitative verification while beingexpressive enough to be useful in modelling and analysis of real timesystems. A number of tools for analysis of timed automata have beenimplemented and applied in industrial scale case studies.Our proposed research is to pursue the exploration of efficientalgorithmic methods for (stochastic) quantitative real time synthesiswith models based on timed automata. More specifically, we plan towork on computational complexity and algorithms for solving 2-playergames with quantitative objectives played on timed automata and othersubclasses of hybrid systems.
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.warwick.ac.uk