Bounded Model Checking with Description Logic Reasoning View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2007-01-01

AUTHORS

Shoham Ben-David , Richard Trefler , Grant Weddell

ABSTRACT

Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system.Description Logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description Logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\cal{ALCI}$\end{document}. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT + + , significantly improve on a previous approach that used DL reasoning for model checking. More... »

PAGES

60-72

Book

TITLE

Automated Reasoning with Analytic Tableaux and Related Methods

ISBN

978-3-540-73098-9
978-3-540-73099-6

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-73099-6_7

DOI

http://dx.doi.org/10.1007/978-3-540-73099-6_7

DIMENSIONS

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


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/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "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"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "David R. Cheriton School of Computer Science, University of Waterloo", 
          "id": "http://www.grid.ac/institutes/grid.46078.3d", 
          "name": [
            "David R. Cheriton School of Computer Science, University of Waterloo"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ben-David", 
        "givenName": "Shoham", 
        "id": "sg:person.014277266142.27", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014277266142.27"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "David R. Cheriton School of Computer Science, University of Waterloo", 
          "id": "http://www.grid.ac/institutes/grid.46078.3d", 
          "name": [
            "David R. Cheriton School of Computer Science, University of Waterloo"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Trefler", 
        "givenName": "Richard", 
        "id": "sg:person.014157474701.53", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014157474701.53"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "David R. Cheriton School of Computer Science, University of Waterloo", 
          "id": "http://www.grid.ac/institutes/grid.46078.3d", 
          "name": [
            "David R. Cheriton School of Computer Science, University of Waterloo"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Weddell", 
        "givenName": "Grant", 
        "id": "sg:person.01111756132.29", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01111756132.29"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2007-01-01", 
    "datePublishedReg": "2007-01-01", 
    "description": "Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system.Description Logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description Logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect \\documentclass[12pt]{minimal}\n\t\t\t\t\\usepackage{amsmath}\n\t\t\t\t\\usepackage{wasysym}\n\t\t\t\t\\usepackage{amsfonts}\n\t\t\t\t\\usepackage{amssymb}\n\t\t\t\t\\usepackage{amsbsy}\n\t\t\t\t\\usepackage{mathrsfs}\n\t\t\t\t\\usepackage{upgreek}\n\t\t\t\t\\setlength{\\oddsidemargin}{-69pt}\n\t\t\t\t\\begin{document}$\\cal{ALCI}$\\end{document}. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT\u2009+\u2009+\u2009, significantly improve on a previous approach that used DL reasoning for model checking.", 
    "editor": [
      {
        "familyName": "Olivetti", 
        "givenName": "Nicola", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-540-73099-6_7", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-73098-9", 
        "978-3-540-73099-6"
      ], 
      "name": "Automated Reasoning with Analytic Tableaux and Related Methods", 
      "type": "Book"
    }, 
    "keywords": [
      "natural settings", 
      "reasoning", 
      "description logics", 
      "representation", 
      "logic reasoning", 
      "dialects", 
      "problem", 
      "model", 
      "checking", 
      "family", 
      "setting", 
      "model checking", 
      "knowledge representation formalism", 
      "representation formalism", 
      "concurrent systems", 
      "previous approaches", 
      "error", 
      "Bounded Model", 
      "finite-state concurrent systems", 
      "compact representation", 
      "description logic reasoning", 
      "logic", 
      "assignment", 
      "results", 
      "CNF formulas", 
      "fact", 
      "approach", 
      "unfolding", 
      "BMC problem", 
      "description", 
      "SAT solvers", 
      "consistency problem", 
      "one", 
      "system", 
      "respect", 
      "satisfying assignments", 
      "experimental results", 
      "tableau technique", 
      "model description", 
      "specification", 
      "technique", 
      "solver", 
      "depth", 
      "size", 
      "formalism", 
      "formulation", 
      "formula", 
      "DL dialect", 
      "DL reasoner FaCT", 
      "reasoner FaCT"
    ], 
    "name": "Bounded Model Checking with Description Logic Reasoning", 
    "pagination": "60-72", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1048623224"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-540-73099-6_7"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-540-73099-6_7", 
      "https://app.dimensions.ai/details/publication/pub.1048623224"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2021-12-01T20:00", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20211201/entities/gbq_results/chapter/chapter_226.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-540-73099-6_7"
  }
]
 

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-540-73099-6_7'

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-540-73099-6_7'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-73099-6_7'

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-540-73099-6_7'


 

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

124 TRIPLES      23 PREDICATES      75 URIs      68 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-540-73099-6_7 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author Nd4b59cd75ae2415c93adc0cf4983bc11
4 schema:datePublished 2007-01-01
5 schema:datePublishedReg 2007-01-01
6 schema:description Model checking is a technique for verifying that a finite-state concurrent system is correct with respect to its specification. In bounded model checking (BMC), the system is unfolded until a given depth, and translated into a CNF formula. A SAT solver is then applied to the CNF formula, to find a satisfying assignment. Such a satisfying assignment, if found, demonstrates an error in the model of the concurrent system.Description Logic (DL) is a family of knowledge representation formalisms, for which reasoning is based on tableaux techniques. We show how Description Logic can serve as a natural setting for representing and solving a BMC problem. We formulate a bounded model checking problem as a consistency problem in the DL dialect \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$\cal{ALCI}$\end{document}. Our formulation results in a compact representation of the model, one that is linear in the size of the model description, and does not involve any unfolding of the model. Experimental results, using the DL reasoner FaCT + + , significantly improve on a previous approach that used DL reasoning for model checking.
7 schema:editor Nfa1c545c7034456e85eff0311047d6ed
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree true
11 schema:isPartOf N64f98317ffca4d64951e3945aa14e747
12 schema:keywords BMC problem
13 Bounded Model
14 CNF formulas
15 DL dialect
16 DL reasoner FaCT
17 SAT solvers
18 approach
19 assignment
20 checking
21 compact representation
22 concurrent systems
23 consistency problem
24 depth
25 description
26 description logic reasoning
27 description logics
28 dialects
29 error
30 experimental results
31 fact
32 family
33 finite-state concurrent systems
34 formalism
35 formula
36 formulation
37 knowledge representation formalism
38 logic
39 logic reasoning
40 model
41 model checking
42 model description
43 natural settings
44 one
45 previous approaches
46 problem
47 reasoner FaCT
48 reasoning
49 representation
50 representation formalism
51 respect
52 results
53 satisfying assignments
54 setting
55 size
56 solver
57 specification
58 system
59 tableau technique
60 technique
61 unfolding
62 schema:name Bounded Model Checking with Description Logic Reasoning
63 schema:pagination 60-72
64 schema:productId N1072b29dbfed40b5b972ceccb0a7d628
65 Nb100912c5e744087bcccd5d4af84be67
66 schema:publisher Nede06ce5819046f8a25e5412150c7037
67 schema:sameAs https://app.dimensions.ai/details/publication/pub.1048623224
68 https://doi.org/10.1007/978-3-540-73099-6_7
69 schema:sdDatePublished 2021-12-01T20:00
70 schema:sdLicense https://scigraph.springernature.com/explorer/license/
71 schema:sdPublisher N5793d80f5c3344ff8036dc30d5151b47
72 schema:url https://doi.org/10.1007/978-3-540-73099-6_7
73 sgo:license sg:explorer/license/
74 sgo:sdDataset chapters
75 rdf:type schema:Chapter
76 N1072b29dbfed40b5b972ceccb0a7d628 schema:name dimensions_id
77 schema:value pub.1048623224
78 rdf:type schema:PropertyValue
79 N5793d80f5c3344ff8036dc30d5151b47 schema:name Springer Nature - SN SciGraph project
80 rdf:type schema:Organization
81 N64f98317ffca4d64951e3945aa14e747 schema:isbn 978-3-540-73098-9
82 978-3-540-73099-6
83 schema:name Automated Reasoning with Analytic Tableaux and Related Methods
84 rdf:type schema:Book
85 N73a16d47227e4490929a40f19e8a65c5 schema:familyName Olivetti
86 schema:givenName Nicola
87 rdf:type schema:Person
88 N9635409296994af6beaa10fe390ef612 rdf:first sg:person.01111756132.29
89 rdf:rest rdf:nil
90 Na5ce04825d434f7a85c84da90badd938 rdf:first sg:person.014157474701.53
91 rdf:rest N9635409296994af6beaa10fe390ef612
92 Nb100912c5e744087bcccd5d4af84be67 schema:name doi
93 schema:value 10.1007/978-3-540-73099-6_7
94 rdf:type schema:PropertyValue
95 Nd4b59cd75ae2415c93adc0cf4983bc11 rdf:first sg:person.014277266142.27
96 rdf:rest Na5ce04825d434f7a85c84da90badd938
97 Nede06ce5819046f8a25e5412150c7037 schema:name Springer Nature
98 rdf:type schema:Organisation
99 Nfa1c545c7034456e85eff0311047d6ed rdf:first N73a16d47227e4490929a40f19e8a65c5
100 rdf:rest rdf:nil
101 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
102 schema:name Information and Computing Sciences
103 rdf:type schema:DefinedTerm
104 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
105 schema:name Computation Theory and Mathematics
106 rdf:type schema:DefinedTerm
107 sg:person.01111756132.29 schema:affiliation grid-institutes:grid.46078.3d
108 schema:familyName Weddell
109 schema:givenName Grant
110 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01111756132.29
111 rdf:type schema:Person
112 sg:person.014157474701.53 schema:affiliation grid-institutes:grid.46078.3d
113 schema:familyName Trefler
114 schema:givenName Richard
115 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014157474701.53
116 rdf:type schema:Person
117 sg:person.014277266142.27 schema:affiliation grid-institutes:grid.46078.3d
118 schema:familyName Ben-David
119 schema:givenName Shoham
120 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.014277266142.27
121 rdf:type schema:Person
122 grid-institutes:grid.46078.3d schema:alternateName David R. Cheriton School of Computer Science, University of Waterloo
123 schema:name David R. Cheriton School of Computer Science, University of Waterloo
124 rdf:type schema:Organization
 




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


...