transparent gif

 

Ej inloggad.

Göteborgs universitets publikationer

SAT-Solving in Practice, with a Tutorial Example from Supervisory Control

Författare och institution:
Koen Claessen (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers), Chalmers); Niklas Een (-); Mary Sheeran (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers), Chalmers); Niklas Sörensson (Institutionen för data- och informationsteknik (GU)); Alexey Voronov (Institutionen för signaler och system, Automation, Chalmers); Knut Åkesson (Institutionen för signaler och system, Automation, Chalmers)
Publicerad i:
Discrete Event Dynamic Systems, 19 ( 4 ) s. 495-524
ISSN:
0924-6703
Publikationstyp:
Artikel, refereegranskad vetenskaplig
Publiceringsår:
2009
Språk:
engelska
Fulltextlänk:
Fulltextlänk (lokalt arkiv):
Sammanfattning (abstract):
Satisfiability solving, the problem of deciding whether the variables of a propositional formula can be assigned in such a way that the formula evaluates to true, is one of the classic problems in computer science. It is of theoretical interest because it is the canonical NP-complete problem. It is of practical interest because modern SAT-solvers can be used to solve many important and practical problems. In this tutorial paper, we show briefly how such SAT-solvers are implemented, and point to some typical applications of them. Our aim is to provide sufficient information (much of it through the reference list) to kick-start researchers from new fields wishing to apply SAT-solvers to their problems. Supervisory control theory originated within the control community and is a framework for reasoning about a plant to be controlled and a specification that the closed-loop system must fulfil. This paper aims to bridge the gap between the computer science community and the control community by illustrating how SAT-based techniques can be used to solve some supervisory control related problems.
Ämne (baseras på Högskoleverkets indelning av forskningsämnen):
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi)
NATURVETENSKAP ->
Data- och informationsvetenskap ->
Datavetenskap (datalogi) ->
Teoretisk datalogi
Nyckelord:
Formal verification, Boolean satisfiability problem, Model checking, Supervisory control
Chalmers styrkeområden:
Informations- och kommunikationsteknik
Produktion
Postens nummer:
98185
Ingår i post nr:
Posten skapad:
2009-09-16 15:59
Posten ändrad:
2016-07-01 13:47

Visa i Endnote-format

Göteborgs universitet • Tel. 031-786 0000
© Göteborgs universitet 2007