計(jì)算機(jī)科學(xué)中的邏輯

LogicinComputerScience

YongmeiLiu

ymliu@

Dept,ofComputerScience

SunYat-senUniversity

December14,2009

Y.LiuLogicinComputerScience1/41

Introductionandoutline

FocusonapplicationsoflogicincomputerScience

JSATsolversandapplications

JProgramverification

」Modelchecking

口Cognitiverobotics

Y.LiuLogicinComputerScience2/41

Amotivatingexample

WewouldliketoselectpeoplefromAnn,Bob,CarolandDanfora

certainjob.Thefollowingconstraintsmustbesatisfied:

■BoborCarolshouldbeselected

aAnnandDancannotbebothselected

aIfBobisselected,Danshouldalsobeselected

Howshouldweselectthepeople?

(6Vc)A(-?QV「d)AVd)

{B,D}

Whatifwehavemanypeopleandmanyconstraints?

Y.LiuLogicinComputerScience3/41

WhatisSAT?

aAliteralisanatomorthenegationofanatom

aAclauseisadisjunctionofliterals

aAformulaisinConjunctiveNormalForm(CNF)ifitisa

conjunctionofclauses

aExample:(5Vc)A(->aV->d)A(T)Vd)

flSAT:GivenapropositionalformulainCNF,decideifthere

existsatruthassignmentthatsatisfiestheformula

Y.LiuLogicinComputerScience4/41

Timecomplexityofalgorithms

Expressedintermsofthenumberofoperationsused

aDecideifatruthassignmentsatisfiesaCNFformula:O(m)

aNaivealgorithmtosolveSAT:O^2nm)

n-thenumberofatoms,m-thelengthoftheformula

Thecomputertimeusedbyalgorithms

ProblemSizeBitOperationsUsed

nnnlog/7n12”

103X10-9s10-8s3XIO-8sKT?5|o-6§

IO27x10-9$10-7§7x)0"7sIO_5s4X10"yr

1031(0X10%IO-6s1X10-5sICT?§*

IO4l(3XIO-8sIO-s1X10-%10Ts*

IO5l(7xIO-8sIO_4s2XIO_3s10s?

IO62x10-8$10-3$2X10-%17min*

*:morethanIO100years

Y.LiuLogicinComputerScience5/41

Pvs.NP

aP:theclassofproblemsforwhichthereexistsaprocedure

thatrunsinpolynomialtime

aExample:decideifatruthassignmentsatisfiesaformula

flNP:theclassofproblemswherewearesearchingforanitem

inalargespaceofpossibilities,butwherewecantestifa

candidateitemisasolutioninpolynomialtime

aExample:decideifapropositionalformulaissatisfiable

■P=NP?OneofthesevenMillenniumPrizeProblems

selectedbytheClayMathematicsInstitutetocarryaUS$

1,000,000prizeforthefirstcorrectsolution.

aItisgenerallyacceptedthatP*NP

Y.LiuLogicinComputerScience6/41

NPCompleteness

aAproblemisNP-completeifitisinNPandanyproblemin

NPcanbereducedtoitinpolynomialtime

aifanyNP-completeproblemisinP,thenP=NP

aSATisaclassicalNP-completeproblem,soanyproblemin

NPcanbereducedtoSATinpolytime

aTherearethousandsofcomputationalproblemsofeconomic

significancethatareknowntobeinNP

aStephenCookreceivedthe1982Turingawardforhisworkon

NP-completeness

Y.LiuLogicinComputerScience7/41

TheDPLLprocedure

NamedaftertheauthorsDavis,Putnam,Logemann,andLoveland

dpll(F):

JIfthesetofclausesFisempty,return1

JIfFcontainsanemptyclause,return0

JIfFcontainsaunitclauseMtreturndpl(M,F)

asimplifyFusingM,getG,returndpll(G)

hJChooseanatomA

Jreturndpl(A,F)Vdpl(->A,F)

Example:(feVc)A(->QV->d)A(-Vd)

CompleteSATsolver

Y.LiuLogicinComputerScience8/41

TheGSATprocedure

aWestartwitharandomtruthassignmenttoallatoms,

aandthenstartchangingthetruthofcertainatomsuntil

aweeitherobtainasatisfyingassignmentorgiveupandtry

again(uptoamaximum)

aGSAToftenoutperformsdpll

aIncompleteSATsolver

Y.LiuLogicinComputerScience9/41

ProgressofSATsolvers

a1960-2010,about50yearshistory

■1995-2010,significantgrowthandsuccessinSATsolver,

researchbasedonDPLL

aThenumberofvariables:10—>106

aManypracticalapplicationsemerged,pushsolverstotheir

limits,andmotivatemoreefficientalgorithm

aNewtechniquesforSATsolversemergeoneaftertheother

aGRASP(1996):thepioneerof2ndgenerationofSATsolver

aCHAFF(2001):carefulengineeringallaspectsofthesearch

Y.LiuLogicinComputerScience10/41

TheN-queensproblem

GivenNqueensandanNxNchessboard,

findawayofplacingthosequeensinsuch

awaythatnoneofthemcanattackanyof

theothers.

eachqueenmustbe

onitsown

,row

?column

,leftdiagonal\

?rightdiagonal/

Y.LiuLogicinComputerScience11/41

EncodingtheN-queensinSAT

Weillustratethecasewheren=8

Introduce8x8atomsp?jsaying

"thereisaqueenatrowiandcolumnj”

aThereisatleast1queenoneveryrow

AL1Vj=lPij

aThereisatmost1queenoneveryrow

Ai=lAj=lAfc=J+lVrpik)

aThereisatleast1queenoneverycolumn

aThereisatmost1queenoneverycolumn

aThereisatmost1queenoneveryleftdiagonal

aThereisatmost1queenoneveryrightdiagonal

Y.LiuLogicinComputerScience12/41

RunningtheN-queens

Ingeneral,theprocedureweuseisthis:

1.wereadtheprobleminput(inthiscase,justn)

2.weconstructtheclausalformulaF

3.wecallaSATsolver

4.wetranslatethesatisfyingtruthassignment

backintothedesiredproblemoutput

Allbutstep(3)shouldbedoneinpolynomialtime.

FortheN-queens,ifwerunaSATsolverforn=8,we

willgetbackatruthassignmentwithexactly8ofthe

64atomstrue.

onesuchisthefollowing:

Pll'P25,P3*P46'P53'P72'PM

(thisisthefirstsolutioninleft-to-rightorder)

Fornlargerthan20or30,dpssrunsintodifficulties

Butgsatcansolvetheseforninthethousands.

Y.LiuLogicinComputerScience13/41

SudokupuzzlerrFn

Givenapartiallyfilled9x9

gridT,fillTwithdigitss.t.L7—LLi

I1ri

aeachcolumn,4

aeachrow,L_j

aeachofthenine3x3Kr

sub-grids28

containsallofthedigitsfromLLL6j

1to9.

Y.LiuLogicinComputerScience14/41

EncodingSudokuinSAT

Introduce9x9atoms:sxyzdenotesfilling(x,y)withdigitz

a(x,y)hasbeenfilledwithz:sxyz

aEachgridcanbefilledwithatmostonedigit

Ax=lA?；=1Az=lAc=z+1(「SsyzVF"如)

aEachdigitappearsatleastonceineachcolumn

A：=lAz=lVx=lSxyz

aEachdigitappearsatleastonceineachrow

Ax=l及Z=\V；=lSXyz

aEachdigitappearsatleastonceineach3x3sub-grid

/\i=0A/=0/\x=lAy=lVz=：lS(3e+i)(3j+g)z

□?《閆

室><考，

Y.LiuLogicinComputerScience15/41

Outline

iJSATsolversandapplications

hJProgramverification

,JModelchecking

hJCognitiverobotics

Y.LiuLogicinComputerScience16/41

Amotivatingexample

Socomputestheintegerdivisionofxandy

1.a:=0;

2.b:=x;

3.while(b>=y)do

4.b:=b-y;

5.a:=a+1;

6.od

Howtoensureourselvesthattheprogramiscorrect?

Y.LiuLogicinComputerScience17/41

Hoarelogic

aIn1969,Hoareintroducedanaxiomaticmethodofproving

programcorrectness

aHoareintroducedthenotationof{p}S{(/}(calledHoare

triples),whereSisaprogram,andp,qareformulasina

first-orderlanguage.

aTheintuitivemeaningof{p}S{(/}:ifpholdsbeforethe

executionofSandtheexecutionofSterminates,thenq

holdsafterwards.

Y.LiuLogicinComputerScience18/41

Aproofsystem

」AssignmentAxiom

{pQ/。}立：=t{p},

JCompositionRule

{p}Si{r},{r}S2{q}

{p}5i；52{<?}'

■if-then-elseRule

{p八e}Si{q},{pAf}S?{q}

{p}ifethenS\elseS?fi{q}

.JwhileRule

_______{pAe}S{p}_______

{p}whileedoSod{pA-?e}

hlConsequenceRule

PTPl,{Pl}S{qi},qiTq

{0}S{q},

Y.LiuLogicinComputerScience19/41

Anexampleproof

Wewanttoprove{x>0A>0}S(){Q-y+b=x/\0<b<y}

ByComp,itsufficestoprovethefollowing:

(1){x>Q/\y>0}a:=0]b:=x{a-y+b=x/\0<b}

Cons(3,6)

(3)rr>0A7/>0—>0-?/+rr=3rA0<:r

(4){0①}a:=0{a-y+x=xf\0<x}Assn

(5){a?yx=x/\0<x}b:=x{a-yb=x/\0<b}Assn

(6){0?y+1=①A0W①}a:=0]b:=x{a-y-\-b=x/\0<b}

Comp(4r5)

(2){a-y+b=x/\0<b}whileloop{a-y+b=x/\0<b<y}

Thekeyistofindtheloopinvarianta-yb=x/\0<b

Y.LiuLogicinComputerScience20/41

Anexampleproof(2)

Wenowprove

(2){a-yb=x/\0<b}whileloop{a-y-\-b=x/\0<b<y}

ByWhile,itsufficestoprove

(7){a-y-^-b=x/\0<b/\b>y}

b:=b—y;a:=a+1{a-yh=xf\0<h}Cons(8,ll)

(8)a-y+b=x/\0<b/\b>y—>(a^iyy+b—y=x/\b-y>0

(9){(a+l)-y+6—y=a:A5—y>0}b:=b—y

{(a+l).g+b=i八吐0}Assn

(10){(a+l)-y+b=xA6>0}a:=a+l

{a-y-\-b=x/\b>0}Assn

(11){(a+l)-y+b—y=x/\b-y>0}b:=b—y;a:=a+1

{a'yb=x/\b>0}Comp(9,10)

Y.LiuLogicinComputerScience21/41

Outline

iJSATsolversandapplications

」Programverification

」Modelchecking

hJCognitiverobotics

Y.LiuLogicinComputerScience22/41

Amotivatingexample

aWhenconcurrentprocessessharearesource,wemayneedto

ensurethattheydonothaveaccesstoitatthesametime.

aForexample,wedonotwantseveralprocessestoeditthe

samefileatthesametime.

aWeidentifycertaincriticalsectionsofeachprocess*code,and

ensurethatonlyoneprocesscanbeinitscriticalsectionata

time.

aWewanttofindaprotocolfordeterminingwhichprocessis

allowedtoenteritscriticalsectionatwhichtime.

Y.LiuLogicinComputerScience23/41

Desiredpropertiesoftheprotocol

」Safety:onlyoneprocessisinitscriticalsectionatanytime.

」Liveness:wheneveranyprocessrequeststoenteritscritical

section,itwilleventuallybepermittedtodoso.

」Non-blocking:aprocesscanalwaysrequesttoenterits

criticalsection.

」Nostrictsequencing:processesneednotentertheircritical

sectioninstrictsequence.

Y.LiuLogicinComputerScience24/41

Threecomponentsofaformalverificationtechnique

」Aframeworkformodelingsystems

QAspecificationlanguagefordescribingsystemproperties

」Anautomaticverificationmethodtoestablishwhetherthe

systemmodelsatisfiesthespecification

Y.LiuLogicinComputerScience25/41

Amodelformutualexclusion

Eachprocesshas3states:n(non-criticalstate),

t(tryingtoentercriticalstate),c(criticalstate)

Y.LiuLogicinComputerScience26/41

AtransitionsystemM=(S,—L)

■asetofstatesS

■atransitionrelation—>(abinaryrelationonS)

■foreverys￡Shassomes'eSwiths—>s'

■alabelingfunctionL:StP(Atoms)

1OQC

Y.LiuLogicinComputerScience27/41

Unwindingatransitionsystemtoaninfinitetree

Linear-timetemporallogic

a0：：=p|-|0|0A歐|X，|F（j）|G（j）|0U歐

apisanypropositionalatom

aXmeans4neXtstate,

aFmeans'someFuturestate1

■Gmeans"allfuturestates（Globally）^

aUmeans'until'

Y.LiuLogicinComputerScience29/41

Branching-timelogic:CTL

.0::=p|w0A@|AX（j）IEX6IAF（I）IEF@\

AG。|EG@|A[（j）U^]|司型

aAmeans4forAllpaths'

aEmeans*thereExistsonepath,

0><&）><復(fù)*<建>>W）AC

Y.LiuLogicinComputerScience30/41

Representingthepropertiesintemporallogic

」Safety:onlyoneprocessisinitscriticalsectionatanytime.

AC2)

口Liveness:wheneveranyprocessrequeststoenteritscritical

section,itwilleventuallybepermittedtodoso.

G(ti—>Fei)AG&2tFC2)

」Non-blocking:Aprocesscanalwaysrequeststoenterits

criticalsection.

4Gdi-EXti)A4Gs2-EXt2)

」Nostrictsequencing:processesneednotentertheircritical

sectioninstrictsequence.

EF?A(->5AE[->C2(7CI])])

Y.LiuLogicinComputerScience31/41

Verifyingtheproperties

9G-|(C1AC2),TfCi)AG2TFc2)

aAG(mtEXti)AAG{n2tEXg)

aEF(c\AE[ciU(-*ciAE[-iC2Uci])]]

Y.LiuLogicinComputerScience32/41

Modelcheckingalgorithms

aCheckwhetheragiventransitionsystemsatisfiesagiven

temporalformula

aLTLandCTLmodelcheckingcanbedoneintime。⑹，

wherenisthesizeofthetransitionsystem

aThestateexplosionproblem:thesizeofthetransitionsystem

isexponentialinthenumberofstatevariables

aApproacheshavebeendevelopedtocombattheproblem

asymbolicmodelchecking

aboundedmodelchecking

aClarke,Emerson,andSifakissharedthe2007TuringAward

fortheirworkonmodelchecking.

Y.LiuLogicinComputerScience33/41

Outline

iJSATsolversandapplications

」Programverification

,JModelchecking

JCognitiverobotics

Y.LiuLogicinComputerScience34/41

Roboticsvs.cognitiverobotics

aRoboticshastraditionallyemphasizedlow-levelsensingand

controltasksincludingsensoryprocessing,pathplanning,and

manipulatordesignandcontrol.

aCognitiveroboticsisconcernedwithendowingrobotsand

softwareagentswithhigherlevelcognitivefunctionsthat

enablethemtoreason,actandperceiveinchanging,

incompletelyknown,andunpredictableenvironments.

aSuchrobotsmust,forexample,beabletoreasonaboutgoals,

actions,whentoperceiveandwhattolookfor,thecognitive

statesofotheragents,etc.

Y.LiuLogicinComputerScience35/41

Cognitiverobotics

aThestudyofknowledgerepresentationandreasoning

problemsfacedbyanautonomousrobot(oragent)ina

dynamicandincompletelyknownworld.

aCentraltothiseffortistodevelopanunderstandingofthe

relationshipbetweentheknowledge,theperception,andthe

actionofsucharobot.

aThegoalishigh-levelroboticcontrol:developasystemthatis

capableofgeneratingactionsintheworldthatareappropriate

asafunctionofsomecurrentsetofbeliefsanddesires.

Y.LiuLogicinComputerScience36/41

Representingadynamicworld:situationcalculus

aActions:puton(x、y)andputonTable(x)

aSituations:S。,do{puton(C,A),So),

aFluents:on(C,D,So),A,do(puton(C^A),So))

aActionpreconditionaxioms:

Poss(puton(x、y),s)=clear(x)Aclear(y\

aSuccessorStateAxioms:

O7z(c,y,do(a,s))三Q=puton(x,y)V

y、s)A->a=putonTable(x)A~^(3z)a=pn,t(m(x,z),

Y.LiuLogicinComputerScience37/41

Twobasicreasoningtasks

LJTh