References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt145",{id:"formSmash:upper:j_idt145",widgetVar:"widget_formSmash_upper_j_idt145",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt146_j_idt148",{id:"formSmash:upper:j_idt146:j_idt148",widgetVar:"widget_formSmash_upper_j_idt146_j_idt148",target:"formSmash:upper:j_idt146:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

Logics and Algorithms for Verification of Concurrent SystemsPrimeFaces.cw("AccordionPanel","widget_formSmash_some",{id:"formSmash:some",widgetVar:"widget_formSmash_some",multiple:true}); PrimeFaces.cw("AccordionPanel","widget_formSmash_all",{id:"formSmash:all",widgetVar:"widget_formSmash_all",multiple:true});
function selectAll()
{
var panelSome = $(PrimeFaces.escapeClientId("formSmash:some"));
var panelAll = $(PrimeFaces.escapeClientId("formSmash:all"));
panelAll.toggle();
toggleList(panelSome.get(0).childNodes, panelAll);
toggleList(panelAll.get(0).childNodes, panelAll);
}
/*Toggling the list of authorPanel nodes according to the toggling of the closeable second panel */
function toggleList(childList, panel)
{
var panelWasOpen = (panel.get(0).style.display == 'none');
// console.log('panel was open ' + panelWasOpen);
for (var c = 0; c < childList.length; c++) {
if (childList[c].classList.contains('authorPanel')) {
clickNode(panelWasOpen, childList[c]);
}
}
}
/*nodes have styleClass ui-corner-top if they are expanded and ui-corner-all if they are collapsed */
function clickNode(collapse, child)
{
if (collapse && child.classList.contains('ui-corner-top')) {
// console.log('collapse');
child.click();
}
if (!collapse && child.classList.contains('ui-corner-all')) {
// console.log('expand');
child.click();
}
}
PrimeFaces.cw("AccordionPanel","widget_formSmash_responsibleOrgs",{id:"formSmash:responsibleOrgs",widgetVar:"widget_formSmash_responsibleOrgs",multiple:true}); 2012 (English)Doctoral thesis, comprehensive summary (Other academic)
##### Abstract [en]

##### Place, publisher, year, edition, pages

Uppsala: Acta Universitatis Upsaliensis, 2012. , 48 p.
##### Series

Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 964
##### National Category

Computer Science
##### Research subject

Computer Science
##### Identifiers

URN: urn:nbn:se:uu:diva-179847ISBN: 978-91-554-8447-7OAI: oai:DiVA.org:uu-179847DiVA: diva2:546861
##### Public defence

2012-10-01, Room 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
##### Opponent

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt375",{id:"formSmash:j_idt375",widgetVar:"widget_formSmash_j_idt375",multiple:true});
##### Supervisors

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt381",{id:"formSmash:j_idt381",widgetVar:"widget_formSmash_j_idt381",multiple:true});
#####

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt387",{id:"formSmash:j_idt387",widgetVar:"widget_formSmash_j_idt387",multiple:true});
Available from: 2012-09-11 Created: 2012-08-24 Last updated: 2014-07-21Bibliographically approved
##### List of papers

In this thesis we investigate how the known framework of automatic formal verification by model checking can be extended in different directions. One extension is to go beyond the common limitation of the existing specification formalisms, that they can describe only regular properties of components. This can be achieved using logics capable of expressing non-regular properties, such as the Propositional Dynamic Logic of Context-free Programs (PDL_{CF}), Fixpoint Logic with Chop (FLC) or the Higher-order Fixpoint Logic (HFL). Our main result in this area is proving that the problem of model checking HFL formulas of order bounded by *k* is *k*-EXPTIME complete. In the proofs we demonstrate two model checking algorithms for that logic. We also show that PDL_{CF} is equivalent to a proper fragment of FLC.

The standard model checking algorithms, which are run on a single computer, are severely limited by the amount of available computing resources. A way to overcome this limitation is to develop distributed algorithms, which can be run on a cluster of computers and use their joint resources. In this thesis we show how a distributed model checking algorithm for the alternation-free fragment of the modal μ-calculus can be extended to handle formulas with one level of alternation. This is an important extension, since Lμ formulas with one level of alternation can express the same properties as logics LTL and CTL commonly used in formal verification.

Finally, we investigate stochastic games which can be used to model additional aspects of components, such as their interaction with environment and their quantitative properties. We describe new algorithms for finding optimal values and strategies in turn-based stochastic games with reachability winning conditions. We prove their correctness and report on experiments where we compare them against each other and against other known algorithms, such as value iteration and strategy improvement.

1. Parallel model checking for LTL, CTL* and Lmu2$(function(){PrimeFaces.cw("OverlayPanel","overlay76574",{id:"formSmash:j_idt423:0:j_idt427",widgetVar:"overlay76574",target:"formSmash:j_idt423:0:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

2. The Complexity of Model Checking Higher Order Fixpoint Logic$(function(){PrimeFaces.cw("OverlayPanel","overlay108038",{id:"formSmash:j_idt423:1:j_idt427",widgetVar:"overlay108038",target:"formSmash:j_idt423:1:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

3. Propositional dynamic logic of context-free programs and fixpoint logic with chop$(function(){PrimeFaces.cw("OverlayPanel","overlay233845",{id:"formSmash:j_idt423:2:j_idt427",widgetVar:"overlay233845",target:"formSmash:j_idt423:2:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

4. The Complexity of Model Checking Higher-order Fixpoint Logic$(function(){PrimeFaces.cw("OverlayPanel","overlay233843",{id:"formSmash:j_idt423:3:j_idt427",widgetVar:"overlay233843",target:"formSmash:j_idt423:3:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

5. Accelerated Approximation for Stochastic Reachability Games: Extended version of paper *New algorithms for solving simple stochastic games*$(function(){PrimeFaces.cw("OverlayPanel","overlay546649",{id:"formSmash:j_idt423:4:j_idt427",widgetVar:"overlay546649",target:"formSmash:j_idt423:4:partsLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

References$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1088",{id:"formSmash:lower:j_idt1088",widgetVar:"widget_formSmash_lower_j_idt1088",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:referencesLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1089_j_idt1091",{id:"formSmash:lower:j_idt1089:j_idt1091",widgetVar:"widget_formSmash_lower_j_idt1089_j_idt1091",target:"formSmash:lower:j_idt1089:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});