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

Direct link
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. , 61 p.
Keyword [en]
Datalogi, fixpoint engine, model checking, tabled resolution, Constraint Logic Programming, strategies
Keyword [sv]
National Category
Computer Science
URN: urn:nbn:se:liu:diva-109ISRN: LITH-IDA-EX--05/056--SEOAI: diva2:17455
Available from: 2005-09-15 Created: 2005-09-15

Open Access in DiVA

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

By organisation
Department of Computer and Information Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 357 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

Total: 325 hits
ReferencesLink to record
Permanent link

Direct link