Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2016-08-03

AUTHORS

Benoît Barbot , Nicolas Basset , Marc Beunardeau , Marta Kwiatkowska

ABSTRACT

Monte Carlo model checking introduced by Smolka and Grosu is an approach to analyse non-probabilistic models using sampling and draw conclusions with a given confidence interval by applying statistical inference. Though not exhaustive, the method enables verification of complex models, even in cases where the underlying problem is undecidable. In this paper we develop Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, as opposed to isotropic sampling that chooses the next step uniformly at random. The uniformity is defined with respect to volume measure of timed languages previously studied by Asarin, Basset and Degorre. We improve over their work by employing a zone graph abstraction instead of the region graph abstraction and incorporating uniform sampling within a zone-based Monte Carlo model checking framework. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical language inclusion measurement in terms of volume. More... »

PAGES

175-190

Book

TITLE

Quantitative Evaluation of Systems

ISBN

978-3-319-43424-7
978-3-319-43425-4

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-319-43425-4_13

DOI

http://dx.doi.org/10.1007/978-3-319-43425-4_13

DIMENSIONS

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


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/01", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Mathematical Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0104", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Statistics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Barbot", 
        "givenName": "Beno\u00eet", 
        "id": "sg:person.011566260657.69", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011566260657.69"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Basset", 
        "givenName": "Nicolas", 
        "id": "sg:person.014372542370.01", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014372542370.01"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "\u00c9cole Normale Sup\u00e9rieure, Paris, France", 
          "id": "http://www.grid.ac/institutes/grid.5607.4", 
          "name": [
            "Ingenico Labs, Paris, France", 
            "\u00c9cole Normale Sup\u00e9rieure, Paris, France"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Beunardeau", 
        "givenName": "Marc", 
        "id": "sg:person.013370624565.99", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013370624565.99"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, University of Oxford, Oxford, UK", 
          "id": "http://www.grid.ac/institutes/grid.4991.5", 
          "name": [
            "Department of Computer Science, University of Oxford, Oxford, UK"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kwiatkowska", 
        "givenName": "Marta", 
        "id": "sg:person.011375012273.39", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2016-08-03", 
    "datePublishedReg": "2016-08-03", 
    "description": "Monte Carlo model checking introduced by Smolka and Grosu is an approach to analyse non-probabilistic models using sampling and draw conclusions with a given confidence interval by applying statistical inference. Though not exhaustive, the method enables verification of complex models, even in cases where the underlying problem is undecidable. In this paper we develop Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, as opposed to isotropic sampling that chooses the next step uniformly at random. The uniformity is defined with respect to volume measure of timed languages previously studied by Asarin, Basset and Degorre. We improve over their work by employing a zone graph abstraction instead of the region graph abstraction and incorporating uniform sampling within a zone-based Monte Carlo model checking framework. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical language inclusion measurement in terms of volume.", 
    "editor": [
      {
        "familyName": "Agha", 
        "givenName": "Gul", 
        "type": "Person"
      }, 
      {
        "familyName": "Van Houdt", 
        "givenName": "Benny", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-319-43425-4_13", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-319-43424-7", 
        "978-3-319-43425-4"
      ], 
      "name": "Quantitative Evaluation of Systems", 
      "type": "Book"
    }, 
    "keywords": [
      "graph abstraction", 
      "model checking", 
      "tool PRISM", 
      "Timed Automata", 
      "non-probabilistic model", 
      "uniform random sampling", 
      "uniform sampling", 
      "abstraction", 
      "complex models", 
      "quantitative properties", 
      "language", 
      "next step", 
      "checking", 
      "Smolka", 
      "algorithm", 
      "SageMath", 
      "Asarin", 
      "verification", 
      "automata", 
      "framework", 
      "model", 
      "statistical inference", 
      "terms of volume", 
      "COSMOS", 
      "isotropic sampling", 
      "applications", 
      "inference", 
      "random sampling", 
      "technique", 
      "sampling", 
      "work", 
      "step", 
      "method", 
      "usefulness", 
      "terms", 
      "respect", 
      "measures", 
      "behavior", 
      "Basset", 
      "cases", 
      "volume", 
      "measurements", 
      "properties", 
      "volume measures", 
      "intervals", 
      "prism", 
      "uniformity", 
      "Monte Carlo model", 
      "inclusion measurements", 
      "confidence intervals", 
      "Carlo model", 
      "conclusion", 
      "Grosu", 
      "approach", 
      "problem", 
      "paper", 
      "Monte Carlo model checking", 
      "Carlo model checking", 
      "Degorre", 
      "zone graph abstraction", 
      "region graph abstraction", 
      "zone-based Monte Carlo model", 
      "statistical language inclusion measurement", 
      "language inclusion measurement"
    ], 
    "name": "Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement", 
    "pagination": "175-190", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1020057572"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-319-43425-4_13"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-319-43425-4_13", 
      "https://app.dimensions.ai/details/publication/pub.1020057572"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-11-01T19:00", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211101/entities/gbq_results/chapter/chapter_413.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-319-43425-4_13"
  }
]
 

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-319-43425-4_13'

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-43425-4_13'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-319-43425-4_13'

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-43425-4_13'


 

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

154 TRIPLES      23 PREDICATES      89 URIs      82 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-319-43425-4_13 schema:about anzsrc-for:01
2 anzsrc-for:0104
3 schema:author N48b87a453e6e4e75b25fafc79efcf244
4 schema:datePublished 2016-08-03
5 schema:datePublishedReg 2016-08-03
6 schema:description Monte Carlo model checking introduced by Smolka and Grosu is an approach to analyse non-probabilistic models using sampling and draw conclusions with a given confidence interval by applying statistical inference. Though not exhaustive, the method enables verification of complex models, even in cases where the underlying problem is undecidable. In this paper we develop Monte Carlo model checking techniques to evaluate quantitative properties of timed languages. Our approach is based on uniform random sampling of behaviours, as opposed to isotropic sampling that chooses the next step uniformly at random. The uniformity is defined with respect to volume measure of timed languages previously studied by Asarin, Basset and Degorre. We improve over their work by employing a zone graph abstraction instead of the region graph abstraction and incorporating uniform sampling within a zone-based Monte Carlo model checking framework. We implement our algorithms using tools PRISM, SageMath and COSMOS, and demonstrate their usefulness on statistical language inclusion measurement in terms of volume.
7 schema:editor Nd26383fccd2947a7be378d1930eb0548
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf Ne92fcb2d49d0468aa5fe0d3b3837b35b
12 schema:keywords Asarin
13 Basset
14 COSMOS
15 Carlo model
16 Carlo model checking
17 Degorre
18 Grosu
19 Monte Carlo model
20 Monte Carlo model checking
21 SageMath
22 Smolka
23 Timed Automata
24 abstraction
25 algorithm
26 applications
27 approach
28 automata
29 behavior
30 cases
31 checking
32 complex models
33 conclusion
34 confidence intervals
35 framework
36 graph abstraction
37 inclusion measurements
38 inference
39 intervals
40 isotropic sampling
41 language
42 language inclusion measurement
43 measurements
44 measures
45 method
46 model
47 model checking
48 next step
49 non-probabilistic model
50 paper
51 prism
52 problem
53 properties
54 quantitative properties
55 random sampling
56 region graph abstraction
57 respect
58 sampling
59 statistical inference
60 statistical language inclusion measurement
61 step
62 technique
63 terms
64 terms of volume
65 tool PRISM
66 uniform random sampling
67 uniform sampling
68 uniformity
69 usefulness
70 verification
71 volume
72 volume measures
73 work
74 zone graph abstraction
75 zone-based Monte Carlo model
76 schema:name Uniform Sampling for Timed Automata with Application to Language Inclusion Measurement
77 schema:pagination 175-190
78 schema:productId N6d873dc9922c4269912c0786df87a370
79 N7a9844de92a3479eb8bd55ebefb07d88
80 schema:publisher N200cce1c1c8e4bbb934804311045aefb
81 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020057572
82 https://doi.org/10.1007/978-3-319-43425-4_13
83 schema:sdDatePublished 2021-11-01T19:00
84 schema:sdLicense https://scigraph.springernature.com/explorer/license/
85 schema:sdPublisher Nc003be6618994ec49404bf176f85bb7e
86 schema:url https://doi.org/10.1007/978-3-319-43425-4_13
87 sgo:license sg:explorer/license/
88 sgo:sdDataset chapters
89 rdf:type schema:Chapter
90 N1b059c6e1ccf4ca191f33d1f34faa427 schema:familyName Agha
91 schema:givenName Gul
92 rdf:type schema:Person
93 N200cce1c1c8e4bbb934804311045aefb schema:name Springer Nature
94 rdf:type schema:Organisation
95 N2d0d8f9484234988adfad046cf208970 rdf:first sg:person.014372542370.01
96 rdf:rest N895e9ed4ca0b49faa43e7798637909be
97 N48b87a453e6e4e75b25fafc79efcf244 rdf:first sg:person.011566260657.69
98 rdf:rest N2d0d8f9484234988adfad046cf208970
99 N6d873dc9922c4269912c0786df87a370 schema:name dimensions_id
100 schema:value pub.1020057572
101 rdf:type schema:PropertyValue
102 N7a9844de92a3479eb8bd55ebefb07d88 schema:name doi
103 schema:value 10.1007/978-3-319-43425-4_13
104 rdf:type schema:PropertyValue
105 N87af9fdd46c04858b5d19aa6a06798df rdf:first sg:person.011375012273.39
106 rdf:rest rdf:nil
107 N895e9ed4ca0b49faa43e7798637909be rdf:first sg:person.013370624565.99
108 rdf:rest N87af9fdd46c04858b5d19aa6a06798df
109 N8b1af60e3ad34a3ebbc0b63e6b132ac9 schema:familyName Van Houdt
110 schema:givenName Benny
111 rdf:type schema:Person
112 N8e18b2ea5e584c408ba681191efc205a rdf:first N8b1af60e3ad34a3ebbc0b63e6b132ac9
113 rdf:rest rdf:nil
114 Nc003be6618994ec49404bf176f85bb7e schema:name Springer Nature - SN SciGraph project
115 rdf:type schema:Organization
116 Nd26383fccd2947a7be378d1930eb0548 rdf:first N1b059c6e1ccf4ca191f33d1f34faa427
117 rdf:rest N8e18b2ea5e584c408ba681191efc205a
118 Ne92fcb2d49d0468aa5fe0d3b3837b35b schema:isbn 978-3-319-43424-7
119 978-3-319-43425-4
120 schema:name Quantitative Evaluation of Systems
121 rdf:type schema:Book
122 anzsrc-for:01 schema:inDefinedTermSet anzsrc-for:
123 schema:name Mathematical Sciences
124 rdf:type schema:DefinedTerm
125 anzsrc-for:0104 schema:inDefinedTermSet anzsrc-for:
126 schema:name Statistics
127 rdf:type schema:DefinedTerm
128 sg:person.011375012273.39 schema:affiliation grid-institutes:grid.4991.5
129 schema:familyName Kwiatkowska
130 schema:givenName Marta
131 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011375012273.39
132 rdf:type schema:Person
133 sg:person.011566260657.69 schema:affiliation grid-institutes:grid.4991.5
134 schema:familyName Barbot
135 schema:givenName Benoît
136 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011566260657.69
137 rdf:type schema:Person
138 sg:person.013370624565.99 schema:affiliation grid-institutes:grid.5607.4
139 schema:familyName Beunardeau
140 schema:givenName Marc
141 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.013370624565.99
142 rdf:type schema:Person
143 sg:person.014372542370.01 schema:affiliation grid-institutes:grid.4991.5
144 schema:familyName Basset
145 schema:givenName Nicolas
146 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014372542370.01
147 rdf:type schema:Person
148 grid-institutes:grid.4991.5 schema:alternateName Department of Computer Science, University of Oxford, Oxford, UK
149 schema:name Department of Computer Science, University of Oxford, Oxford, UK
150 rdf:type schema:Organization
151 grid-institutes:grid.5607.4 schema:alternateName École Normale Supérieure, Paris, France
152 schema:name Ingenico Labs, Paris, France
153 École Normale Supérieure, Paris, France
154 rdf:type schema:Organization
 




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


...