uu.seUppsala University Publications

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_upper_j_idt150",{id:"formSmash:upper:j_idt150",widgetVar:"widget_formSmash_upper_j_idt150",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:upper:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_upper_j_idt151_j_idt153",{id:"formSmash:upper:j_idt151:j_idt153",widgetVar:"widget_formSmash_upper_j_idt151_j_idt153",target:"formSmash:upper:j_idt151:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});

The Complexity of Model Checking Higher-order Fixpoint LogicPrimeFaces.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}); 2007 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 3, no 2:7, 1-33 p.Article in journal (Refereed) Published
##### Abstract [en]

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

2007. Vol. 3, no 2:7, 1-33 p.
##### Keyword [en]

mu-calculis, lambda-calculus, model checking, complexity
##### National Category

Computer and Information Science
##### Identifiers

URN: urn:nbn:se:uu:diva-107983DOI: 10.2168/lmcs-3(2:7)2007ISI: 000262497200006OAI: oai:DiVA.org:uu-107983DiVA: diva2:233843
#####

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

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

PrimeFaces.cw("AccordionPanel","widget_formSmash_j_idt468",{id:"formSmash:j_idt468",widgetVar:"widget_formSmash_j_idt468",multiple:true});
Available from: 2009-09-02 Created: 2009-09-02 Last updated: 2017-12-13Bibliographically approved
##### In thesis

Higher-Order Fixpoint Logic (HFL) is a hybrid of the simply typed λ-calculus and the modal μ-calculus. This makes it a highly expressive temporal logic that is capable of expressing various interesting correctness properties of programs that are not expressible in the modal μ-calculus. This paper provides complexity results for its model checking problem. In particular we consider those fragments of HFL built by using only types of bounded order *k* and arity *m*. We establish *k*-fold exponential time completeness for model checking each such fragment. For the upper bound we use fixpoint elimination to obtain reachability games that are singly-exponential in the size of the formula and *k*-fold exponential in the size of the underlying transition system. These games can be solved in deterministic linear time. As a simple consequence, we obtain an exponential time upper bound on the expression complexity of each such fragment. The lower bound is established by a reduction from the word problem for alternating *(k-1)*-fold exponential space bounded Turing Machines. Since there are fixed machines of that type whose word problems are already hard with respect to *k*-fold exponential time, we obtain, as a corollary, *k*-fold exponential time completeness for the data complexity of our fragments of HFL, provided *m* exceeds 3. This also yields a hierarchy result in expressive power.

1. Logics and Algorithms for Verification of Concurrent Systems$(function(){PrimeFaces.cw("OverlayPanel","overlay546861",{id:"formSmash:j_idt729:0:j_idt733",widgetVar:"overlay546861",target:"formSmash:j_idt729:0:parentLink",showEvent:"mousedown",hideEvent:"mousedown",showEffect:"blind",hideEffect:"fade",appendToBody:true});});

doi
urn-nbn$(function(){PrimeFaces.cw("Tooltip","widget_formSmash_j_idt1174",{id:"formSmash:j_idt1174",widgetVar:"widget_formSmash_j_idt1174",showEffect:"fade",hideEffect:"fade",showDelay:500,hideDelay:300,target:"formSmash:altmetricDiv"});});

CiteExport$(function(){PrimeFaces.cw("TieredMenu","widget_formSmash_lower_j_idt1227",{id:"formSmash:lower:j_idt1227",widgetVar:"widget_formSmash_lower_j_idt1227",autoDisplay:true,overlay:true,my:"left top",at:"left bottom",trigger:"formSmash:lower:exportLink",triggerEvent:"click"});}); $(function(){PrimeFaces.cw("OverlayPanel","widget_formSmash_lower_j_idt1228_j_idt1230",{id:"formSmash:lower:j_idt1228:j_idt1230",widgetVar:"widget_formSmash_lower_j_idt1228_j_idt1230",target:"formSmash:lower:j_idt1228:permLink",showEffect:"blind",hideEffect:"fade",my:"right top",at:"right bottom",showCloseIcon:true});});