Counting CTL View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2010

AUTHORS

François Laroussinie , Antoine Meyer , Eudes Petonnet

ABSTRACT

This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and of the complexity of their model-checking problem (ranging from P-complete to undecidable). More... »

PAGES

206-220

Book

TITLE

Foundations of Software Science and Computational Structures

ISBN

978-3-642-12031-2
978-3-642-12032-9

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-642-12032-9_15

DOI

http://dx.doi.org/10.1007/978-3-642-12032-9_15

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1045419482


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

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 d'Informatique Algorithmique: Fondements et Applications", 
          "id": "https://www.grid.ac/institutes/grid.462842.e", 
          "name": [
            "LIAFA, Universit\u00e9 Paris Diderot \u2013 Paris 7 & CNRS UMR, 7089, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Laroussinie", 
        "givenName": "Fran\u00e7ois", 
        "id": "sg:person.013052027213.09", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013052027213.09"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Laboratoire d'Informatique Gaspard-Monge", 
          "id": "https://www.grid.ac/institutes/grid.462940.d", 
          "name": [
            "LIGM, Universit\u00e9 Paris Est \u2013 Marne-la-Valle & CNRS UMR, 8049, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Meyer", 
        "givenName": "Antoine", 
        "id": "sg:person.012233570403.65", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012233570403.65"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Laboratoire d'Informatique Algorithmique: Fondements et Applications", 
          "id": "https://www.grid.ac/institutes/grid.462842.e", 
          "name": [
            "LIAFA, Universit\u00e9 Paris Diderot \u2013 Paris 7 & CNRS UMR, 7089, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Petonnet", 
        "givenName": "Eudes", 
        "id": "sg:person.013626531403.05", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013626531403.05"
        ], 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.1007/3-540-11494-7_22", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1002397064", 
          "https://doi.org/10.1007/3-540-11494-7_22"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/199448.199470", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1004679622"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf00355298", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006145660", 
          "https://doi.org/10.1007/bf00355298"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf00355298", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1006145660", 
          "https://doi.org/10.1007/bf00355298"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1006/inco.1993.1024", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1008470395"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/b978-0-444-88074-1.50021-4", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1011407656"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1006/inco.1999.2817", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1012629852"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0019-9958(83)80051-5", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013356942"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0019-9958(83)80051-5", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1013356942"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/j.tcs.2005.11.020", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1016673812"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-46691-6_9", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1022006801", 
          "https://doi.org/10.1007/3-540-46691-6_9"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-46691-6_9", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1022006801", 
          "https://doi.org/10.1007/3-540-46691-6_9"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-60692-0_70", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1022695129", 
          "https://doi.org/10.1007/3-540-60692-0_70"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/s0304-3975(02)00644-8", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1027543458"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bfb0030596", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1037133129", 
          "https://doi.org/10.1007/bfb0030596"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bfb0025774", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1037700041", 
          "https://doi.org/10.1007/bfb0025774"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-58179-0_50", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1045256125", 
          "https://doi.org/10.1007/3-540-58179-0_50"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/772062.772064", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1045370349"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-45315-6_21", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1048122397", 
          "https://doi.org/10.1007/3-540-45315-6_21"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-45315-6_21", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1048122397", 
          "https://doi.org/10.1007/3-540-45315-6_21"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/244795.244803", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1050750695"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1109/sfcs.1977.32", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1086187044"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1109/lics.1995.523250", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1093348997"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1109/lics.1999.782628", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1093797076"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "2010", 
    "datePublishedReg": "2010-01-01", 
    "description": "This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and of the complexity of their model-checking problem (ranging from P-complete to undecidable).", 
    "editor": [
      {
        "familyName": "Ong", 
        "givenName": "Luke", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-642-12032-9_15", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-642-12031-2", 
        "978-3-642-12032-9"
      ], 
      "name": "Foundations of Software Science and Computational Structures", 
      "type": "Book"
    }, 
    "name": "Counting CTL", 
    "pagination": "206-220", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1045419482"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-642-12032-9_15"
        ]
      }, 
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "d85a6209ed00730187e8c2b665d317bae73350a3395b1c5a133ad549a66aa2cd"
        ]
      }
    ], 
    "publisher": {
      "location": "Berlin, Heidelberg", 
      "name": "Springer Berlin Heidelberg", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-642-12032-9_15", 
      "https://app.dimensions.ai/details/publication/pub.1045419482"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2019-04-16T07:30", 
    "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/0000000356_0000000356/records_57883_00000000.jsonl", 
    "type": "Chapter", 
    "url": "https://link.springer.com/10.1007%2F978-3-642-12032-9_15"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

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-642-12032-9_15'

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-642-12032-9_15'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-642-12032-9_15'

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-642-12032-9_15'


 

This table displays all metadata directly associated to this object as RDF triples.

150 TRIPLES      23 PREDICATES      47 URIs      20 LITERALS      8 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-642-12032-9_15 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nf9e1b31d399f4aaa83180fb0b2f4e4f5
4 schema:citation sg:pub.10.1007/3-540-11494-7_22
5 sg:pub.10.1007/3-540-45315-6_21
6 sg:pub.10.1007/3-540-46691-6_9
7 sg:pub.10.1007/3-540-58179-0_50
8 sg:pub.10.1007/3-540-60692-0_70
9 sg:pub.10.1007/bf00355298
10 sg:pub.10.1007/bfb0025774
11 sg:pub.10.1007/bfb0030596
12 https://doi.org/10.1006/inco.1993.1024
13 https://doi.org/10.1006/inco.1999.2817
14 https://doi.org/10.1016/b978-0-444-88074-1.50021-4
15 https://doi.org/10.1016/j.tcs.2005.11.020
16 https://doi.org/10.1016/s0019-9958(83)80051-5
17 https://doi.org/10.1016/s0304-3975(02)00644-8
18 https://doi.org/10.1109/lics.1995.523250
19 https://doi.org/10.1109/lics.1999.782628
20 https://doi.org/10.1109/sfcs.1977.32
21 https://doi.org/10.1145/199448.199470
22 https://doi.org/10.1145/244795.244803
23 https://doi.org/10.1145/772062.772064
24 schema:datePublished 2010
25 schema:datePublishedReg 2010-01-01
26 schema:description This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and of the complexity of their model-checking problem (ranging from P-complete to undecidable).
27 schema:editor Ne7017a4a22894bee9a770e78e7a6065b
28 schema:genre chapter
29 schema:inLanguage en
30 schema:isAccessibleForFree true
31 schema:isPartOf N2255d220befb4d8fa854a915b1ee6ab5
32 schema:name Counting CTL
33 schema:pagination 206-220
34 schema:productId N4688231ff6e54d8fb526adec59204c37
35 Nc69c44a8a8384a04bb42a89e4d6e0a9a
36 Nfaeec2b77c464985aad629464889e01e
37 schema:publisher Nbe307377b13e418cb7d962e3647b4660
38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045419482
39 https://doi.org/10.1007/978-3-642-12032-9_15
40 schema:sdDatePublished 2019-04-16T07:30
41 schema:sdLicense https://scigraph.springernature.com/explorer/license/
42 schema:sdPublisher Nad58b039fccf4f74834c51aaf694aacd
43 schema:url https://link.springer.com/10.1007%2F978-3-642-12032-9_15
44 sgo:license sg:explorer/license/
45 sgo:sdDataset chapters
46 rdf:type schema:Chapter
47 N2255d220befb4d8fa854a915b1ee6ab5 schema:isbn 978-3-642-12031-2
48 978-3-642-12032-9
49 schema:name Foundations of Software Science and Computational Structures
50 rdf:type schema:Book
51 N4423efc7f8a4461bbd6338e086f39766 rdf:first sg:person.013626531403.05
52 rdf:rest rdf:nil
53 N4688231ff6e54d8fb526adec59204c37 schema:name doi
54 schema:value 10.1007/978-3-642-12032-9_15
55 rdf:type schema:PropertyValue
56 N7c8ddd2e88df4d5fa509296ac5b2f839 schema:familyName Ong
57 schema:givenName Luke
58 rdf:type schema:Person
59 N92a52feff1234223b19103eacac1f5e1 rdf:first sg:person.012233570403.65
60 rdf:rest N4423efc7f8a4461bbd6338e086f39766
61 Nad58b039fccf4f74834c51aaf694aacd schema:name Springer Nature - SN SciGraph project
62 rdf:type schema:Organization
63 Nbe307377b13e418cb7d962e3647b4660 schema:location Berlin, Heidelberg
64 schema:name Springer Berlin Heidelberg
65 rdf:type schema:Organisation
66 Nc69c44a8a8384a04bb42a89e4d6e0a9a schema:name readcube_id
67 schema:value d85a6209ed00730187e8c2b665d317bae73350a3395b1c5a133ad549a66aa2cd
68 rdf:type schema:PropertyValue
69 Ne7017a4a22894bee9a770e78e7a6065b rdf:first N7c8ddd2e88df4d5fa509296ac5b2f839
70 rdf:rest rdf:nil
71 Nf9e1b31d399f4aaa83180fb0b2f4e4f5 rdf:first sg:person.013052027213.09
72 rdf:rest N92a52feff1234223b19103eacac1f5e1
73 Nfaeec2b77c464985aad629464889e01e schema:name dimensions_id
74 schema:value pub.1045419482
75 rdf:type schema:PropertyValue
76 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
77 schema:name Information and Computing Sciences
78 rdf:type schema:DefinedTerm
79 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
80 schema:name Computation Theory and Mathematics
81 rdf:type schema:DefinedTerm
82 sg:person.012233570403.65 schema:affiliation https://www.grid.ac/institutes/grid.462940.d
83 schema:familyName Meyer
84 schema:givenName Antoine
85 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012233570403.65
86 rdf:type schema:Person
87 sg:person.013052027213.09 schema:affiliation https://www.grid.ac/institutes/grid.462842.e
88 schema:familyName Laroussinie
89 schema:givenName François
90 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013052027213.09
91 rdf:type schema:Person
92 sg:person.013626531403.05 schema:affiliation https://www.grid.ac/institutes/grid.462842.e
93 schema:familyName Petonnet
94 schema:givenName Eudes
95 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013626531403.05
96 rdf:type schema:Person
97 sg:pub.10.1007/3-540-11494-7_22 schema:sameAs https://app.dimensions.ai/details/publication/pub.1002397064
98 https://doi.org/10.1007/3-540-11494-7_22
99 rdf:type schema:CreativeWork
100 sg:pub.10.1007/3-540-45315-6_21 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048122397
101 https://doi.org/10.1007/3-540-45315-6_21
102 rdf:type schema:CreativeWork
103 sg:pub.10.1007/3-540-46691-6_9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022006801
104 https://doi.org/10.1007/3-540-46691-6_9
105 rdf:type schema:CreativeWork
106 sg:pub.10.1007/3-540-58179-0_50 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045256125
107 https://doi.org/10.1007/3-540-58179-0_50
108 rdf:type schema:CreativeWork
109 sg:pub.10.1007/3-540-60692-0_70 schema:sameAs https://app.dimensions.ai/details/publication/pub.1022695129
110 https://doi.org/10.1007/3-540-60692-0_70
111 rdf:type schema:CreativeWork
112 sg:pub.10.1007/bf00355298 schema:sameAs https://app.dimensions.ai/details/publication/pub.1006145660
113 https://doi.org/10.1007/bf00355298
114 rdf:type schema:CreativeWork
115 sg:pub.10.1007/bfb0025774 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037700041
116 https://doi.org/10.1007/bfb0025774
117 rdf:type schema:CreativeWork
118 sg:pub.10.1007/bfb0030596 schema:sameAs https://app.dimensions.ai/details/publication/pub.1037133129
119 https://doi.org/10.1007/bfb0030596
120 rdf:type schema:CreativeWork
121 https://doi.org/10.1006/inco.1993.1024 schema:sameAs https://app.dimensions.ai/details/publication/pub.1008470395
122 rdf:type schema:CreativeWork
123 https://doi.org/10.1006/inco.1999.2817 schema:sameAs https://app.dimensions.ai/details/publication/pub.1012629852
124 rdf:type schema:CreativeWork
125 https://doi.org/10.1016/b978-0-444-88074-1.50021-4 schema:sameAs https://app.dimensions.ai/details/publication/pub.1011407656
126 rdf:type schema:CreativeWork
127 https://doi.org/10.1016/j.tcs.2005.11.020 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016673812
128 rdf:type schema:CreativeWork
129 https://doi.org/10.1016/s0019-9958(83)80051-5 schema:sameAs https://app.dimensions.ai/details/publication/pub.1013356942
130 rdf:type schema:CreativeWork
131 https://doi.org/10.1016/s0304-3975(02)00644-8 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027543458
132 rdf:type schema:CreativeWork
133 https://doi.org/10.1109/lics.1995.523250 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093348997
134 rdf:type schema:CreativeWork
135 https://doi.org/10.1109/lics.1999.782628 schema:sameAs https://app.dimensions.ai/details/publication/pub.1093797076
136 rdf:type schema:CreativeWork
137 https://doi.org/10.1109/sfcs.1977.32 schema:sameAs https://app.dimensions.ai/details/publication/pub.1086187044
138 rdf:type schema:CreativeWork
139 https://doi.org/10.1145/199448.199470 schema:sameAs https://app.dimensions.ai/details/publication/pub.1004679622
140 rdf:type schema:CreativeWork
141 https://doi.org/10.1145/244795.244803 schema:sameAs https://app.dimensions.ai/details/publication/pub.1050750695
142 rdf:type schema:CreativeWork
143 https://doi.org/10.1145/772062.772064 schema:sameAs https://app.dimensions.ai/details/publication/pub.1045370349
144 rdf:type schema:CreativeWork
145 https://www.grid.ac/institutes/grid.462842.e schema:alternateName Laboratoire d'Informatique Algorithmique: Fondements et Applications
146 schema:name LIAFA, Université Paris Diderot – Paris 7 & CNRS UMR, 7089, France
147 rdf:type schema:Organization
148 https://www.grid.ac/institutes/grid.462940.d schema:alternateName Laboratoire d'Informatique Gaspard-Monge
149 schema:name LIGM, Université Paris Est – Marne-la-Valle & CNRS UMR, 8049, France
150 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...