Ontology type: schema:Chapter
2017-08-25
AUTHORSFlorian Bruse , Martin Lange , Etienne Lozes
ABSTRACTHigher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed -calculus into the modal -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most . In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in -EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL. More... »
PAGES26-41
Reachability Problems
ISBN
978-3-319-67088-1
978-3-319-67089-8
http://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3
DOIhttp://dx.doi.org/10.1007/978-3-319-67089-8_3
DIMENSIONShttps://app.dimensions.ai/details/publication/pub.1091344167
JSON-LD is the canonical representation for SciGraph data.
TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT
[
{
"@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json",
"about": [
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Computation Theory and Mathematics",
"type": "DefinedTerm"
},
{
"id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08",
"inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/",
"name": "Information and Computing Sciences",
"type": "DefinedTerm"
}
],
"author": [
{
"affiliation": {
"alternateName": "Laboratoire Sp\u00e9cification et V\u00e9rification",
"id": "https://www.grid.ac/institutes/grid.464035.0",
"name": [
"University of Kassel, Kassel, Germany",
"LSV, ENS Paris-Saclay, CNRS, Cachan, France"
],
"type": "Organization"
},
"familyName": "Bruse",
"givenName": "Florian",
"id": "sg:person.011477555577.66",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011477555577.66"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "University of Kassel",
"id": "https://www.grid.ac/institutes/grid.5155.4",
"name": [
"University of Kassel, Kassel, Germany"
],
"type": "Organization"
},
"familyName": "Lange",
"givenName": "Martin",
"id": "sg:person.013644521143.88",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013644521143.88"
],
"type": "Person"
},
{
"affiliation": {
"alternateName": "Laboratoire Sp\u00e9cification et V\u00e9rification",
"id": "https://www.grid.ac/institutes/grid.464035.0",
"name": [
"LSV, ENS Paris-Saclay, CNRS, Cachan, France"
],
"type": "Organization"
},
"familyName": "Lozes",
"givenName": "Etienne",
"id": "sg:person.014336046241.62",
"sameAs": [
"https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014336046241.62"
],
"type": "Person"
}
],
"citation": [
{
"id": "https://doi.org/10.1017/s0956796800003889",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1009194735"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1017/s0956796800003889",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1009194735"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-28644-8_33",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1010792135",
"https://doi.org/10.1007/978-3-540-28644-8_33"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-28644-8_33",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1010792135",
"https://doi.org/10.1007/978-3-540-28644-8_33"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/3-540-61604-7_60",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1011410166",
"https://doi.org/10.1007/3-540-61604-7_60"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/s0022-0000(70)80006-x",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1017051545"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/0020-0190(87)90097-4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1019521827"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/0020-0190(87)90097-4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1019521827"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/s0304-3975(98)00314-4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1020192627"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/0022-0000(83)90014-4",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1022042880"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/0304-3975(82)90125-6",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1024922185"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/j.jal.2005.08.002",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1035621913"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1016/j.ipl.2006.04.019",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1043145663"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1090/s0002-9947-1965-0170805-7",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1050589417"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-662-44602-7_8",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1052220395",
"https://doi.org/10.1007/978-3-662-44602-7_8"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-75560-9_7",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1053125586",
"https://doi.org/10.1007/978-3-540-75560-9_7"
],
"type": "CreativeWork"
},
{
"id": "sg:pub.10.1007/978-3-540-75560-9_7",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1053125586",
"https://doi.org/10.1007/978-3-540-75560-9_7"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.2168/lmcs-3(2:7)2007",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1069150905"
],
"type": "CreativeWork"
},
{
"id": "https://doi.org/10.1109/focs.1965.11",
"sameAs": [
"https://app.dimensions.ai/details/publication/pub.1086192375"
],
"type": "CreativeWork"
}
],
"datePublished": "2017-08-25",
"datePublishedReg": "2017-08-25",
"description": "Higher-Order Fixpoint Logic (HFL) is a modal specification language whose expressive power reaches far beyond that of Monadic Second-Order Logic, achieved through an incorporation of a typed -calculus into the modal -calculus. Its model checking problem on finite transition systems is decidable, albeit of high complexity, namely k-EXPTIME-complete for formulas that use functions of type order at most . In this paper we present a fragment with a presumably easier model checking problem. We show that so-called tail-recursive formulas of type order k can be model checked in -EXPSPACE, and also give matching lower bounds. This yields generic results for the complexity of bisimulation-invariant non-regular properties, as these can typically be defined in HFL.",
"editor": [
{
"familyName": "Hague",
"givenName": "Matthew",
"type": "Person"
},
{
"familyName": "Potapov",
"givenName": "Igor",
"type": "Person"
}
],
"genre": "chapter",
"id": "sg:pub.10.1007/978-3-319-67089-8_3",
"inLanguage": [
"en"
],
"isAccessibleForFree": false,
"isPartOf": {
"isbn": [
"978-3-319-67088-1",
"978-3-319-67089-8"
],
"name": "Reachability Problems",
"type": "Book"
},
"name": "Space-Efficient Fragments of Higher-Order Fixpoint Logic",
"pagination": "26-41",
"productId": [
{
"name": "doi",
"type": "PropertyValue",
"value": [
"10.1007/978-3-319-67089-8_3"
]
},
{
"name": "readcube_id",
"type": "PropertyValue",
"value": [
"533d033a8ac7d8f9d6a1bad34e00449b8cd3c55423d668092a8c3041b682124b"
]
},
{
"name": "dimensions_id",
"type": "PropertyValue",
"value": [
"pub.1091344167"
]
}
],
"publisher": {
"location": "Cham",
"name": "Springer International Publishing",
"type": "Organisation"
},
"sameAs": [
"https://doi.org/10.1007/978-3-319-67089-8_3",
"https://app.dimensions.ai/details/publication/pub.1091344167"
],
"sdDataset": "chapters",
"sdDatePublished": "2019-04-16T04:59",
"sdLicense": "https://scigraph.springernature.com/explorer/license/",
"sdPublisher": {
"name": "Springer Nature - SN SciGraph project",
"type": "Organization"
},
"sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000325_0000000325/records_100778_00000000.jsonl",
"type": "Chapter",
"url": "https://link.springer.com/10.1007%2F978-3-319-67089-8_3"
}
]Download the RDF metadata as: json-ld nt turtle xml License info
JSON-LD is a popular format for linked data which is fully compatible with JSON.
curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'
N-Triples is a line-based linked data format ideal for batch operations.
curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'
Turtle is a human-readable linked data format.
curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'
RDF/XML is a standard XML format for linked data.
curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-67089-8_3'
This table displays all metadata directly associated to this object as RDF triples.
137 TRIPLES
23 PREDICATES
41 URIs
19 LITERALS
8 BLANK NODES