liu.seSearch for publications in DiVA
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
A CLP(FD)-based model checker for CTL
Linköping University, Department of Computer and Information Science.
2005 (English)Independent thesis Advanced level (degree of Magister), 20 points / 30 hpStudent thesis
Abstract [en]

Model checking is a formal verification method where one tries to prove or disprove properties of a formal system. Typical systems one might want to prove properties within are network protocols and digital circuits. Typical properties to check for are safety (nothing bad ever happens) and liveness (something good eventually happens).

This thesis describes an implementation of a sound and complete model checker for Computation Tree Logic (CTL) using Constraint Logic Programming over Finite Domains (CLP(FD)). The implementation described uses tabled resolution to remember earlier computations, is parameterised by choices of computation strategies and can with slight modification support different constraint domains. Soundness under negation is maintained through a restricted form of constructive negation.

The computation process amounts to a fixpoint search, where a fixpoint is reached when no more extension operations has any effect. As results show, the choice of strategies does influence the efficiency of the computation. Soundness and completeness are of course independent of the choice of strategies. Strategies include how to choose the extension operation for the next step and whether to perform global or local rule instantiations, resulting in bottom-up or top-down computations respectively.

Place, publisher, year, edition, pages
Institutionen för datavetenskap , 2005. , p. 61
Keywords [en]
Datalogi, fixpoint engine, model checking, tabled resolution, Constraint Logic Programming, strategies
Keywords [sv]
Datalogi
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:liu:diva-109ISRN: LITH-IDA-EX--05/056--SEOAI: oai:DiVA.org:liu-109DiVA, id: diva2:17455
Presentation
2005-06-21
Uppsok
teknik
Supervisors
Examiners
Available from: 2005-09-15 Created: 2005-09-15 Last updated: 2018-01-13

Open Access in DiVA

fulltext(514 kB)401 downloads
File information
File name FULLTEXT01.pdfFile size 514 kBChecksum SHA-1
4c959e95a9897a9cf41065fff0d5a88c67fc3c793afcf480164d8f0414b14c301562e621
Type fulltextMimetype application/pdf

By organisation
Department of Computer and Information Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar
Total: 401 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

urn-nbn

Altmetric score

urn-nbn
Total: 403 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • oxford
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf