University of Texas at Dallas
Logic, Infinite Computation,
and Coinduction
Gopal Gupta
Neda Saeedloei, Brian DeVries, Kyle Marple Feliks Kluzniak,
Luke Simon, Ajay Bansal, Ajay Mallya, Richard Min
Applied Logic, Programming-Languages
and Systems (ALPS) Lab
The University of Texas at Dallas
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 1
University of Texas at Dallas
UT Dallas Computer Science
• Located in North Dallas in the middle of Telecom Corridor, home of more
than 600 high tech companies (TI, Alcatel, EDS/HP, ….)
• 45 T/T faculty members; 13 full-time instructors
• 850 UGs, 700 M.S. students, 130 Ph.D. students
• BS/MS/Ph.D. in CS, SE, CE and TE
• 6 Major research areas: AI, Systems, Theory, SE, N/W, Security
• 10 NSF CAREER award winners; 2 Airforce Young Investigators
• $9M research expenditure in 2009-10
• $12 Million new funding in 2010-11
• 40+ grants in 2011-12 totaling more than $12 Million
• UTD ranked 167 now in London Times world ranking
• Recent work on Frankenstein Virus got national/international coverage
• Please consider applying to our Ph.D. program & for faculty positions
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 2
University of Texas at Dallas
Circular Phenomena in Comp. Sci.
• Circularity has dogged Mathematics and Computer
Science ever since Set Theory was first developed:
– The well known Russell’s Paradox:
• R = { x | x is a set that does not contain itself}
Is R contained in R? Yes and No
– Liar Paradox: I am a liar
– Hypergame paradox (Zwicker & Smullyan)
• All these paradoxes involve self-reference through
some type of negation
• Russell put the blame squarely on circularity and
sought to ban it from scientific discourse:
``Whatever involves all of the collection must not be one of
the collection”
-- Russell 1908
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 3
University of Texas at Dallas
Circularity in Computer Science
• Following Russell’s lead, Tarski proposed to ban selfreferential sentences in a language
• Rather, have a hierarchy of languages
• Kripke’s paper challenged this in a1975 paper:
argued that circular phenomenon are far more common and
circularity can’t simply be banned.
• Circularity has been banned from automated theorem
proving and logic programming through the occurs
check rule:
An unbound variable cannot be unified with a term
containing that variable (i.e., X = f(X) not allowed)
• What if we allowed such unification to proceed (as LP
systems always did for efficiency reasons)?
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 4
University of Texas at Dallas
Circularity in Computer Science
• If occurs check is removed, we’ll generate
circular (infinite) structures:
X = [1,2,3 | X]
X = f(X)
• Such structures, of course, arise in computing
(circular linked lists), but banned in logic/LP.
• Subsequent LP systems did allow for such
circular structures (rational terms), but they
only exist as data-structures, there is no proof
theory to go along with it.
– One can hold the data-structure in memory within
an LP execution, but one can’t reason about it.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 5
University of Texas at Dallas
Circularity in Everyday Life
• Circularity arises in every day life
– Most natural phenomenon are cyclical
• Cyclical movement of the earth, moon, etc.
• Our digestive system works in cycles
– Social interactions are cyclical:
• Conversation = (1st speaker, (2nd Speaker, Conversation)
• Shared conventions are cyclical concepts
• Numerous other examples can be found
elsewhere (Barwise & Moss 1996)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 6
University of Texas at Dallas
Circularity in Computer Science
• Circular phenomenon are quite common in
Computer Science:
–
–
–
–
–
–
–
Circular linked lists
Graphs (with cycles)
Controllers (run forever)
Bisimilarity
Interactive systems
Automata over infinite strings/Kripke structures
Perpetual processes
• Logic/LP not equipped to model circularity directly
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 7
University of Texas at Dallas
Coinduction
• Circular structures are infinite structures
X = [1, 2 | X] is logically speaking X = [1, 2, 1, 2, ….]
• Proofs about their properties are infinite-sized
• Coinduction is the technique for proving these
properties
– first proposed by Peter Aczel in the 80s
• Systematic presentation of coinduction & its
application to computing, math. and set theory:
“Vicious Circles” by Moss and Barwise (1996)
• Our focus: inclusion of coinductive reasoning
techniques in LP and theorem proving
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 8
University of Texas at Dallas
Induction vs Coinduction
• Induction is a mathematical technique for finitely
reasoning about an infinite (countable) no. of things.
• Examples of inductive structures:
– Naturals: 0, 1, 2, …
– Lists: [ ], [X], [X, X],
[X, X, X], …
• 3 components of an inductive definition:
(1) Initiality, (2) iteration, (3) minimality
– for example, the set of lists is specified as follows:
[ ] – an empty list is a list (initiality) ……(i)
[H | T] is a list if T is a list and H is an element (iteration) ..(ii)
minimal set that satisfies (i) and (ii) (minimality)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 9
University of Texas at Dallas
Induction vs Coinduction
•
Coinduction is a mathematical technique for
(finitely) reasoning about infinite things.
–
–
–
•
Mathematical dual of induction
If all things were finite, then coinduction would not be
needed.
Perpetual programs, automata over infinite strings
2 components of a coinductive definition:
(1) iteration, (2) maximality
– for example, for a list:
[ H | T ] is a list if T is a list and H is an element (iteration).
Maximal set that satisfies the specification of a list.
– This coinductive interpretation specifies all infinite sized
lists
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 10
University of Texas at Dallas
Example: Natural Numbers
•  (S) = { 0 }  { succ(x) | x  S }
• N = 
– where  is least fixed-point.
• aka “inductive definition”
– Let N be the smallest set such that
• 0N
• x  N implies x + 1  N
• Induction corresponds to Least Fix Point
(LFP) interpretation.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 11
University of Texas at Dallas
Example: Natural Numbers and Infinity
•  (S) = { 0 }  { succ(x) | x  S }
•  unambiguously defines another set
• N’ =  = N  {  }
–  = succ( succ( succ( ... ) ) ) = succ(  ) =  + 1
– where  is a greatest fixed-point
• Coinduction corresponds to Greatest Fixed
Point (GFP) interpretation.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 12
University of Texas at Dallas
Mathematical Foundations
• Duality provides a source of new mathematical tools
that reflect the sophistication of tried and true
techniques.
Definition
Proof tech.
Mapping
Least fixed point
Induction
Recursion
Greatest fixed point
Coinduction
Corecursion
• Co-recursion: recursive def’n without a base case
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 13
University of Texas at Dallas
Applications of Coinduction
•
•
•
•
•
•
•
model checking
bisimilarity proofs
lazy evaluation in FP
reasoning with infinite structures
perpetual processes
cyclic structures
operational semantics of “coinductive logic
programming”
• Type inference systems for lazy functional
languages
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 14
University of Texas at Dallas
Inductive Logic Programming
• Logic Programming
– is actually inductive logic programming.
– has inductive definition.
– useful for writing programs for reasoning about
finite things:
- data structures
- properties
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 15
University of Texas at Dallas
Infinite Objects and Properties
• Traditional logic programming is unable to reason
about infinite objects and/or properties.
• (The glass is only half-full)
• Example: perpetual binary streams
– traditional logic programming cannot handle
bit(0).
bit(1).
bitstream( [ H | T ] ) :- bit( H ), bitstream( T ).
|?- X = [ 0, 1, 1, 0 | X ], bitstream( X ).
• Goal: Combine traditional LP with coinductive LP
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 16
University of Texas at Dallas
Overview of Coinductive LP
• Coinductive Logic Program is
a definite program with maximal co-Herbrand model
declarative semantics.
• Declarative Semantics: across the board dual of
traditional LP:
–
–
–
–
greatest fixed-points
terms: co-Herbrand universe Uco(P)
atoms: co-Herbrand base Bco(P)
program semantics: maximal co-Herbrand model Mco(P).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 17
University of Texas at Dallas
Operational Semantics: co-SLD Resolution
• nondeterministic state transition system
• states are pairs of
– a finite list of syntactic atoms [resolvent] (as in Prolog)
– a set of syntactic term equations of the form x = f(x) or x = t
• For a program p :- p. => the query |?- p. will succeed.
• p( [ 1 | T ] ) :- p( T ). => |?- p(X) to succeed with X= [ 1 | X ].
• transition rules
?-G
– definite clause rule
– “coinductive hypothesis rule”
• if a coinductive goal G is called,
and G unifies with a call made earlier
then G succeeds.
….
G
coinductive
success
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 18
University of Texas at Dallas
Correctness
• Theorem (soundness). If atom A has a
successful co-SLD derivation in program P,
then E(A) is true in program P, where E is the
resulting variable bindings for the derivation.
• Theorem (completeness). If A  Mco(P) has a
rational proof, then A has a successful coSLD derivation in program P.
– Completeness only for rational/regular proofs
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 19
University of Texas at Dallas
Implementation
• Search strategy: hypothesis-first, leftmost, depth-first
• Meta-Interpreter implementation.
query(Goal) :- solve([],Goal).
solve(Hypothesis, (Goal1,Goal2)) :solve( Hypothesis, Goal1), solve(Hypothesis,Goal2).
solve( _ , Atom) :- builtin(Atom), Atom.
solve(Hypothesis,Atom):- member(Atom, Hypothesis).
solve(Hypothesis,Atom):- notbuiltin(Atom),
clause(Atom,Atoms), solve([Atom|Hypothesis],Atoms).
• A complete meta-interpreter available
• Implementation on top of YAP, SWI Prolog available
• Implementation within Logtalk + library of examples
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 20
University of Texas at Dallas
Example: Number Stream
:- coinductive stream/1.
stream( [ H | T ] ) :- num( H ), stream( T ).
num( 0 ).
num( s( N ) ) :- num( N ).
|?- stream( [ 0, s( 0 ), s( s ( 0 ) ) | T ] ).
1.
2.
3.
4.
MEMO: stream( [ 0, s( 0 ), s( s ( 0 ) ) | T ] )
MEMO: stream( [ s( 0 ), s( s ( 0 ) ) | T ] )
MEMO: stream( [ s( s ( 0 ) ) | T ] )
stream(T)
Answers:
T = [ 0, s(0), s(s(0)) | T ]
T = [ 0, s(0), s(s(0)), s(0), s(s(0)) | T ]
T = [ 0, s(0), s(s(0)) | T ] . . .
T = [ 0, s(0), s(s(0)) | X ] (where X is any rational list of numbers.)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 21
University of Texas at Dallas
Example: Append
:- coinductive append/3.
append( [ ], X, X ).
append( [ H | T ], Y, [ H | Z ] ) :- append( T, Y, Z ).
|?- Y = [ 4, 5, 6 | Y ], append( [ 1, 2, 3 ], Y, Z).
Answer: Z = [ 1, 2, 3 | Y ], Y=[ 4, 5, 6 | Y]
|?- X = [ 1, 2, 3 | X ], Y = [ 3, 4 | Y ], append( X, Y, Z).
Answer: Z = [ 1, 2, 3 | Z ].
|?- Z = [ 1, 2 | Z ], append( X, Y, Z ).
Answer: X = [ ], Y = [ 1, 2 | Z ] ;
X = [1, 2 | X], Y = _
X = [ 1 ], Y = [ 2 | Z ] ;
X = [ 1, 2 ], Y = Z; …. ad infinitum
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 22
University of Texas at Dallas
Example: Comember
member(H, [ H | T ]).
member(H, [ X | T ]) :- member(H, T).
?- L = [1,2 | L], member(3, L). succeeds.
Instead:
:- coinductive comember/2. %drop/3 is inductive
comember(X, L) :- drop(X, L, R), comember(X, R).
drop(H, [ H | T ], T).
drop(H, [ X | T ], T1) :- drop(H, T, T1).
?- X=[ 1, 2, 3 | X ], comember(2,X).
Answer: yes.
?- X=[ 1, 2, 3, 1, 2, 3], comember(2, X).
Answer: no.
?- X=[1, 2, 3 | X], comember(Y, X).
Answer: Y = 1;
Y = 2;
Y = 3;
?- X = [1,2 | X], comember(3, X).
Answer: no
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 23
University of Texas at Dallas
Co-Logic Programming
• combines both halves of logic programming:
– traditional logic programming
– coinductive logic programming
• syntactically identical to traditional logic
programming, except predicates are labeled:
– Inductive, or
– coinductive
• and stratification restriction enforced where:
– inductive and coinductive predicates cannot be mutually
recursive. e.g.,
p :- q.
q :- p.
Program rejected, if p coinductive & q inductive
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 24
University of Texas at Dallas
Application of Co-LP
• Co-LP allows one to compute both LFP & GFP
• Computable functions can be specified more elegantly
–
–
–
–
–
–
–
–
Interepreters for Modal Logics can be elegantly specified:
Model Checking: LTL interpreter elegantly specified
Timed -automata: elegantly modeled and properties verified
Modeling/Verification of Cyber Physical Systems/Hybrid automata
Goal-directed execution of Answer Set Programs
Goal-directed SAT solvers (Davis-Putnam like procedure)
Planning under real-time constraints
Operational semantics of the π-calculus (incl. timed π -calculus)
• infinite replication operator modeled with co-induction
Co-LP allows systems to be modeled naturally & elegantly
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 25
University of Texas at Dallas
Application: Model Checking
• automated verification of hardware and software
systems
• -automata
– accept infinite strings
– accepting state must be traversed infinitely often
• requires computation of lfp and gfp
• co-logic programming provides an elegant framework
for model checking
• traditional LP works for safety property (that is based
on lfp) in an elegant manner, but not for liveness .
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 26
University of Texas at Dallas
Verification of Properties
• Types of properties: safety and liveness
• Search for counter-example
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 27
University of Texas at Dallas
Safety versus Liveness
• Safety
– “nothing bad will happen”
– naturally described inductively
– straightforward encoding in traditional LP
• liveness
–
–
–
–
“something good will eventually happen”
dual of safety
naturally described coinductively
straightforward encoding in coinductive LP
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 28
University of Texas at Dallas
Finite Automata
automata([X|T], St):- trans(St, X, NewSt), automata(T, NewSt).
automata([ ], St) :- final(St).
trans(s0, a, s1).
trans(s3, d, s0).
trans(s1, b, s2).
trans(s2, 3, s0).
trans(s2, c, s3).
final(s2).
?- automata(X,s0).
X=[ a, b];
X=[ a, b, e, a, b];
X=[ a, b, e, a, b, e, a, b];
……
……
……
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 29
University of Texas at Dallas
Infinite Automata
automata([X|T], St):- trans(St, X, NewSt), automata(T, NewSt).
trans(s0,a,s1).
trans(s3,d,s0).
trans(s1,b,s2).
trans(s2,3,s0).
trans(s2,c,s3).
final(s2).
?- automata(X,s0).
X=[ a, b, c, d | X ];
X=[ a, b, e | X ];
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 30
University of Texas at Dallas
Verifying Liveness Properties
• Verifying safety properties in LP is relatively easy:
safety modeled by reachability
• Accomplished via tabled logic programming
• Verifying liveness is much harder: a counterexample
to liveness is an infinite trace
• Verifying liveness is transformed into a safety check
via use of negations in model checking and tabled LP
– Considerable overhead incurred
• Co-LP solves the problem more elegantly:
– Infinite traces that serve as counter-examples are produced
as answers
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 31
University of Texas at Dallas
Verifying Liveness Properties
• Consider Safety:
– Question: Is an unsafe state, Su, reachable?
– If answer is yes, the path to Su is the counter-ex.
• Consider Liveness, then dually
– Question: Is a state, D, that should be dead, live?
– If answer is yes, the infinite path containing D is
the counter example
• Co-LP will produce this infinite path as the answer
• Checking for liveness is just as easy as
checking for safety
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 32
University of Texas at Dallas
Nested Finite and Infinite Automata
:- coinductive state/2.
state(s0, [s0,s1 | T]):- enter, work,
state(s1,T).
state(s1, [s1 | T]):- exit, state(s2,T).
state(s2, [s2 | T]):- repeat, state(s0,T).
state(s0, [s0 | T]):- error, state(s3,T).
state(s3, [s3 | T]):- repeat, state(s0,T).
work.
enter. repeat. exit. error.
work :- work.
|?- state(s0,X), absent(s2,X).
X=[ s0, s3 | X ]
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 33
University of Texas at Dallas
An Interpreter for LTL
%--- nots have been pushed to propositions
:- tabled verify/2.
verify(S, [S], A) :- proposition(A), holds(S,A).
%p
verify(S, [S], not(A)) :- proposition(A), \+holds(S,A).
% not(p)
verify(S,P, or(A,B)) :- verify(S, P, A) ; verify(S, P, B). %A or B
verify(S,P, and(A,B)) :- verify(S,P1, A), verify(S,P2, B). %A and B
(prefix(P2, P1), P=P1 ; prefix(P2,P1), P=P2)
verify(S, [S|P], x(A)) :- trans(S, S1), verify(S1, P, A). % X(A)
verify(S, P, f(A)) :- verify(S, P, A); verify(S, P, x(f(A))). % F(A)
verify(S, P, g(A)) :- coverify(S, P, g(A)).
% G(A)
verify(S, P,u(A,B)) :- verify(S, P,B);
verify(S, P,and(A, x(u(A,B)))).
%AuB
verify(S, r(A,B)) :- coverify(S, r(A,B)).
%ArB
:- coinductive coverify/2.
coverify(S, g(A)) :- verify(S, P, and(A, x(g(A))).
coverify(S, r(A,B)) :- verify(S, P, and(A,B)).
coverify(S, r(A,B)) :- verify(S, P, and(B, x(r(A,B)))).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 34
University of Texas at Dallas
Verification of Real-Time Systems
“Train, Controller, Gate”
Timed Automata
• -automata w/ time constrained transitions & stopwatches
• straightforward encoding into CLP(R) + Co-LP
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 35
University of Texas at Dallas
Verification of Real-Time Systems
“Train, Controller, Gate”
:- use_module(library(clpr)).
:- coinductive driver/9.
train(X, up, X, T1,T2,T2).
% up=idle
train(s0,approach,s1,T1,T2,T3) :- {T3=T1}.
train(s1,in,s2,T1,T2,T3):-{T1-T2>2,T3=T2}
train(s2,out,s3,T1,T2,T3).
train(s3,exit,s0,T1,T2,T3):-{T3=T2,T1-T2<5}.
train(X,lower,X,T1,T2,T2).
train(X,down,X,T1,T2,T2).
train(X,raise,X,T1,T2,T2).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 36
University of Texas at Dallas
Verification of Real-Time Systems
“Train, Controller, Gate”
contr(s0,approach,s1,T1,T2,T1).
contr(s1,lower,s2,T1,T2,T3):- {T3=T2, T1-T2=1}.
contr(s2,exit,s3,T1,T2,T1).
contr(s3,raise,s0,T1,T2,T2):-{T1-T2<1}.
contr(X,in,X,T1,T2,T2).
contr(X,up,X,T1,T2,T2).
contr(X,out,X,T1,T2,T2).
contr(X,down,X,T1,T2,T2).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 37
University of Texas at Dallas
Verification of Real-Time Systems
“Train, Controller, Gate”
gate(s0,lower,s1,T1,T2,T3):- {T3=T1}.
gate(s1,down,s2,T1,T2,T3):- {T3=T2,T1-T2<1}.
gate(s2,raise,s3,T1,T2,T3):- {T3=T1}.
gate(s3,up,s0,T1,T2,T3):- {T3=T2,T1-T2>1,T1-T2<2 }.
gate(X,approach,X,T1,T2,T2).
gate(X,in,X,T1,T2,T2).
gate(X,out,X,T1,T2,T2).
gate(X,exit,X,T1,T2,T2).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 38
University of Texas at Dallas
Verification of Real-Time Systems
:- coinductive driver/9.
driver(S0,S1,S2, T,T0,T1,T2, [ X | Rest ], [ (X,T) | R ]) :train(S0,X,S00,T,T0,T00), contr(S1,X,S10,T,T1,T10),
gate(S2,X,S20,T,T2,T20), {TA > T},
driver(S00,S10,S20,TA,T00,T10,T20,Rest,R).
|?- driver(s0,s0,s0,T,Ta,Tb,Tc,X,R).
R=[(approach,A), (lower,B), (down,C), (in,D), (out,E), (exit,F),
(raise,G), (up,H) | R ],
X=[approach, lower, down, in, out, exit, raise, up | X] ;
R=[(approach,A),(lower,B),(down,C),(in,D),(out,E),(exit,F),(raise,G),
(approach,H),(up,I)|R],
X=[approach,lower,down,in,out,exit,raise,approach,up | X] ;
% where A, B, C, ... H, I are the corresponding wall clock time of events generated.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 39
University of Texas at Dallas
DPP – Safety: Deadlock Free
• One potential solution
– Force one philosopher to pick forks
in different order than others
• Checking for deadlock
– Bad state is not reachable
– Implemented using Tabled LP
:- table reach/2.
reach(Si, Sf) :- trans(_,Si,Sf).
reach(Si, Sf) :- trans(_,Si,Sfi),
reach(Sfi,Sf).
?- reach([1,1,1,1,1], [2,2,2,2,2]).
no
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 40
University of Texas at Dallas
DPP – Liveness: Starvation Free
• Phil. waits forever on a fork
• One potential solution
– phil. waiting longest gets the access
– implemented using CLP(R)
• Checking for starvation
– once in bad state, is it possible to
remain there forever?
– implemented using co-LP
?- starved(X).
no
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 41
University of Texas at Dallas
Other Applications
• Advanced -structures can also be modeled and
reasoned about: -PTA and -grammars
• Non monotonic reasoning:
– CoLP allows goal-directed execution of Answer Set
Programs (ASP)
– Abductive reasoners can be elegantly implemented
– Answer sets programming can be extended to predicates
– ASP can be elegantly extended with constraints: advanced
applications such as planning under real-time constraints
become possible
• SAT Solvers can be elegantly written
• Operational semantics of pi-calculus can be given
(infinite replication operator modeled with co-induction)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 42
University of Texas at Dallas
Goal-directed execution of ASP
•
•
•
•
Answer set programming (ASP) is a popular
formalism for non monotonic reasoning
Applications in real-world reasoning, planning, etc.
Semantics given via lfp of a residual program
obtained after “Gelfond-Lifschitz” transform
Popular implementations: Smodels, DLV, etc.
1. No goal-directed execution strategy available
2. ASP limited to only finitely groundable programs
•
•
Co-logic programming solves both these problems.
Also provides a goal-directed method to check if a
proposition is true in some model of a prop. formula
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 43
University of Texas at Dallas
Why Goal-directed ASP?
•
•
•
•
•
•
Most of the time, given a theory, we are interested in
knowing if a particular goal is true or not.
Top down goal-directed execution provides operational
semantics (important for usability)
Execution more efficient.
– Tabled LP vs bottom up Deductive Databases
Why check the consistency of the whole
knowledgebase?
– Inconsistency in some unrelated part will scuttle the whole
system
Most practical examples anyway add a constraint to
force the answer set to contain a certain goal.
– E.g. Zebra puzzle:
:- not satisfied.
Answer sets of non-finitely groundable programs
computable & Constraints incorporated in Prolog style.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 44
University of Texas at Dallas
Negation in Co-LP: co-SLDNF Resolution
• Given a clause such as
p :- q, not p.
?- p. fails coinductively when not p is encountered
• To incorporate negation in coinductive reasoning, need a
negative coinductive hypothesis rule:
– In the process of establishing not(p), if not(p) is seen again in the
resolvent, then not(p) succeeds [co-SLDNF Resolution]
Also, not not p reduces to p.
•
• Answer set programming makes the “glass completely full” by
taking into account failing computations:
•
– p :- q, not p. is consistent if p = false and q = false
However, this takes away monotonicity: q can be constrained to
false, causing q to be withdrawn, if it was established earlier.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 45
University of Texas at Dallas
ASP
• Consider the following program, A:
p :- not q.
t.
r :- t, s.
q :- not p.
s.
A has 2 answer sets: {p, r, t, s} & {q, r, t, s}.
• Now suppose we add the following rule to A:
h :- p, not h.
(falsify p)
Only one answer set remains: {q, r, t, s}
• Gelfond-Lifschitz Method:
– Given an answer set S, for each p  S, delete all rules whose body
contains “not p”;
– delete all goals of the form “not q” in remaining rules
– Compute the least fix point, L, of the residual program
– If S = L, then S is an answer set
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 46
University of Texas at Dallas
Goal-directed ASP
• Consider the following program, A’:
p :- not q.
q :- not p, r.
t.
s.
r :- t, s.
h :- p, not h.
• Separate into constraint and non-constraint rules:
only 1 constraint rule in this case.
• Execute the query under co-LP, candidate answer
sets will be generated.
• Keep the ones not rejected by the constraints.
• Suppose the query is ?- q. Execution: q  not p, r
 not not q, r  q, r  r  t, s  s  success.
Ans = {q, r, t, s}
• Next, we need to check that constraint rules will not
reject the generated answer set.
– (it doesn’t in this case)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 47
University of Texas at Dallas
Goal-directed ASP
• In general, for the constraint rules of p as head,
p1:- B1. p2:- B2. ... pn :- Bn., generate rule(s) of the form:
chk_p1 :- not(p1), B1.
chk_p2 :- not(p2), B2.
...
chk_pn :- not(p), Bn.
• Generate: nmr_chk :- not(chk_p1), ... , not(chk_pn).
• For each pred. definition, generate its negative version:
not_p :- not(B1), not(B2), ... , not(Bn).
• If you want to ask query Q, then ask ?- Q, nmr_chk.
• Execution keeps track of atoms in the answer set (PCHS)
and atoms not in the answer set (NCHS).
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 48
University of Texas at Dallas
Goal-directed ASP
• Consider the following program, P1:
(i) p :- not q.
(ii) q:- not r.
(iii) r :- not p.
P1 has 1 answer set: {q, r}.
(iv) q :- not p.
• Separate into: 3 constraint rules (i, ii, iii)
2 non-constraint rules (i, iv).
p :- not(q). q :- not(r). r :- not(p). q :- not(p).
chk_p :- not(p), not(q). chk_q :- not(q), not(r). chk_r :- not(r), not(p).
nmr_chk :- not(chk_p), not(chk_q), not(chk_r).
not_p :- q. not_q :- r, p. not_r :- p.
Suppose the query is ?- r.
Expand as in co-LP: r  not p  not not q  q (  not r
 fail, backtrack)  not p  success. Ans={r, q} which
satisfies the constraint rules of nmr_chk.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 49
University of Texas at Dallas
Benchmark Results
Top-Down Avg. (s)
Smodels Avg. (s)
Smodels / Top-Down
13 Queens
0.0050
0.0185
3.70
15 Queens
0.0120
0.0760
6.33
19 Queens
0.0235
1.4820
63.06
20 Queens
0.8590
5.3015
6.17
21 Queens
0.0560
19.7560
352.79
22 Queens
7.9100
79.50
10.05
23 Queens
0.1400
216.6700
1547.64
24 Queens
2.0500
101.2400
49.39
8x7 Pigeons
0.0260
0.1515
5.83
11x10 Pigeons
21.0700
131.0700
6.22
10x10 Pigeons
0.0025
0.0055
2.20
20x20 Pigeons
0.0100
0.0790
7.90
30x30 Pigeons
0.0310
0.5155
16.63
40x40 Pigeons
0.0700
2.4340
34.77
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 50
University of Texas at Dallas
Cyber-Physical Systems (CPS)
• CPS:
-- Networked/distributed Hybrid Systems
-- Discrete digital systems with
– Inputs: continuous physical quantities
• e.g., time, distance, acceleration, temperature, etc.
– Outputs: control physical (analog) devices
• Elegantly modeled via co-LP extended with constraints
• Characteristics of CPS:
-- perform discrete computations (modeled via LP)
-- deal with continuous physical quantities (modeled via constraints)
-- are concurrent (modeled via LP coroutining)
-- run forever (modeled via coinduction)
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 51
University of Texas at Dallas
CPS Example
Reactor Temperature Control System
θ = θm
θ = θM
θ = θM
rod2
no_rod
rod1
add2 , c2 := 0 . θ
add1 , c1 := 0 .
. θ
θ
θ = ― - 60
θ = ― - 50
10
θ = ― - 56
10
10
θ
=
θ
θ = θm
m
θm <= θ
θ <= θM
θm <= θ
remove
c
:=
0
2, 2
remove1 , c1 := 0
θ = θM
r1 >= W
r1 = W
add1
in1
r1 := 0
remove1
r2 >= W
r2 = W
shutdown
out1
out2
add2
in2
r2 := 0
remove2
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 52
University of Texas at Dallas
Rod1 & Rod2
trans_r1(out1, add1, in1, T, Ti, To, W)
:{T – Ti >= W, To = Ti}.
trans_r1(in1, remove1, out1, T, Ti, To,
W) :- {To = T}.
trans_r2(out2, add2, in2, T, Ti, To, W)
:{T – Ti >= W, To = Ti}.
trans_r2(in2, remove2, out2, T, Ti, To,
W) :- {To = T}.
r1 >= W
r1 = W
out1
add1
in1
r1 := 0
remove1
r2 >= W
r2 = W
out2
add2
in2
r2 := 0
remove2
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 53
University of Texas at Dallas
Controller
trans_c(norod, add1, rod1, Tetai, Tetao, T, Ti1, Ti2, To1, To2, F) :(F == 1 -> Ti = Ti1; Ti = Ti2),
{Tetai < 550, Tetao = 550, exp(e, (T - Ti)/10) = 5,
To1 = T, To2 = Ti2}.
trans_c(rod1, remove1, norod Tetai, Tetao, T, Ti1, Ti2, To1, To2, F) :{Tetai > 510 Tetao = 510, exp(e, (T - Ti1)/10) = 5,
To1 = T, To2 = Ti2}.
trans_c(norod, add2, rod2, Tetai, Tetao, T, Ti1, Ti2, To1, To2, F) :(F == 1 -> Ti = Ti1; Ti = Ti2),
{Tetai < 550, Tetao = 550, exp(e, (T - Ti)/10) = 5,
To1 = Ti1, To2 = T}.
θ = θm
θ = θM
rod2
no_rod
rod1
add2 , c2 := 0 . θ
add1 , c1 := 0 .
trans_c(rod2, remove2, norod, Tetai, Tetao, T, Ti1, Ti2, To1, To2, F) :-.
θ
θ = ― - 60
θ
θ = ― - 50
{Tetai > 510, Tetao = 510, exp(e, (T - Ti2)/10) = 9/5,
10
θ = ― - 56
10
10
To1 = Ti1, To2 = T}.
θ
=
θ
θ = θm
m
θm <= θ
θ <= θM
θm <= θ
remove2 , c2 := 0
remove1 , c1 := 0
trans_c(norod, _, shutdown, Tetai, Tetao, T, Ti1, Ti2, To1, To2, F) :θ = θM
(F == 1 -> Ti = Ti1; Ti = Ti2),
θ = θM
{Tetai < 550 Tetao = 550, exp(e, (T - Ti)/10) = 5,
To1 = Ti1, To2 = Ti2}.
shutdown
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 54
Controller | Rod1 | Rod2
:- coinductive(contr/7).
contr(X, Si, T, Tetai, Ti1, Ti2, Fi) :(H = add1; H = remove1; H = add2; H = remove2; H = shutdown),
{Ta > T},
freeze(X, contr(Xs, So, Ta, Tetao, To1, To2, Fo)),
trans_c(Si, H, So, Tetai, Tetao, T, Ti1, Ti2, To1, To2, Fi),
((H=add1; H=remove1) -> Fo = 1; Fo = 2),
((H=add1; H=remove1; H=add2; H=remove2) -> X = [ (H, T) | Xs]; X = [ (H, T) ] ).
:- coinductive(rod1/6).
rod1([ (H, T)| Xs], Si1, Si2, Ti1, Ti2, W) :H = add1 ->
freeze(Xs,rod1(Xs, So1, Si2, To1, Ti2, W));
H = remove1 ->
freeze(Xs,rod1(Xs, So1, Si2, To1, Ti2, W);
rod2(Xs, So1, Si2, To1, Ti2, W)),
trans_r1(Si1, H, So1, T, Ti1, To1, W);
H = shutdown -> {T - Ti1 < A, T - Ti2 < A}.
:- coinductive(rod2/6).
rod2([ (H, T)| Xs], Si1, Si2, Ti1, Ti2, W) :H = add2 ->
freeze(Xs,rod2(Xs, Si1, So2, Ti1, To2, W));
H = remove2 ->
freeze(Xs,rod1(Xs, Si1, So2, Ti1, To2, W);
rod2(Xs, Si1, So2, Ti1, To2, W)),
trans_r2(Si2, H, So2, T, Ti2, To2, W);
H = shutdown -> {T - Ti1 < A, T - Ti2 < A}.
University of Texas at Dallas
Controller || Rod1 || Rod2
main(S, T, W) :-
{T - Tr1 = W, T - Tr2 = W},
freeze(S, (rod1(S, s0, s0, Tr1, Tr2, W);
rod2(S, s0, s0, Tr1, Tr2, W))),
contr(S, s0, T, 510, Tc1, Tc2, 1).
• With this elegant modeling, we were able to improve the
bounds on W compared to previous work
• HyTech determines W < 20.44 to prevent shutdown
• Subsequently, using linear hybrid automata with clock
translation, HyTech improves to W < 37.8
• Using our LP method, we refine it to W < 38.06
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 56
University of Texas at Dallas
Related Publications
1. L. Simon, A. Mallya, A. Bansal, and G. Gupta. Coinductive logic
programming. In ICLP’06 .
2. L. Simon, A. Bansal, A. Mallya, and G. Gupta. Co-Logic programming:
Extending logic programming with coinduction. In ICALP’07.
3. G. Gupta et al. Co-LP and its applications, ICLP’07 (tutorial)
4. G. Gupta et al. Infinite computation, coinduction and computational
logic. CALCO’11
5. R. Min, A. Bansal, G. Gupta. Co-LP with negation, LOPSTR 2009
6. R. Min, G. Gupta. Towards Predicate ASP, AIAI’09
7. N. Saeedloei, G. Gupta. Coinductive Constraint Programming
FLOPS12.
8. N. Saeedloei, G. Gupta, Timed π-Calculus
9. N. Saeedloei, G. Gupta. Modeling/verification of CPS with coinductive
coroutined CLP(R)
10. K. Marple, A. Bansal, R. Min, G. Gupta. Goal-directed Execution of
ASP. PPDP’12
11. K. Marple, G. Gupta, Galliwasp: A Goal-Directed Answer Set Solver .
LOPSTR 2012
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 57
University of Texas at Dallas
Conclusion
• Circularity is a common concept in everyday life and
computer science:
• Logic/LP is unable to cope with circularity
• Solution: introduce coinduction in Logic/LP
– dual of traditional logic programming
– operational semantics for coinduction
– combining both halves of logic programming
• applications to verification, non monotonic reasoning,
negation in LP, propositional satisfiability, hybrid
systems, cyberphysical systems
• Goal-directed impl. of non-monotonic reasoning avail.
• Metainterpreter available:
http://www.utdallas.edu/~gupta/meta.tar.gz
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 58
University of Texas at Dallas
Conclusion (cont’d)
• Computation can be classified into two types:
– Well-founded,
• Based on computing elements in the LFP
• Implemented w/ recursion (start from a call, end in base case)
– Consistency-based
• Based on computing elements in the GFP (but not LFP)
• Implemented via co-recursion (look for consistency)
• Combining the two allows one to compute any
computable function elegantly:
– Implementations of modal logics (LTL, etc.)
– Complex reasoning systems (NM reasoners)
• Combining them is challenging
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 59
University of Texas at Dallas
LFP vs GFP
COMPUTATION
G
L
F
P
F
P
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 60
University of Texas at Dallas
LFP vs GFP
COMPUTATION
G
F
P
L
F
P
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 61
University of Texas at Dallas
Conclusions: Future Work
• Design execution strategies that enumerate all rational
infinite solutions while avoiding redundant solutions
p([a|X]) :- p(X).
p([b|X]) :- p(X).
-- If X = [a|X] is reported, then avoid X = [a, a | X], X = [a,a,a|X], etc.
-- A fair depth first search strategy that will produce
X = [a,b|X]
• Combining induction (tabling) and co-induction:
– Stratified co-LP: equivalent to stratified Büchi tree automata
(SBTAs)
– Non-stratified co-LP: inspired by Rabin automata; 3 class of
predicates (i) coinductive, (ii) weakly coinductive and (iii) strongly
coinductive
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 62
University of Texas at Dallas
QUESTIONS?
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 63
University of Texas at Dallas
Coinductive LP: An Example
• Let P1 be the following coinductive program.
:- coinductive from/2.
from(x) = x cons from(x+1)
from( N, [ N | T ] ) :- from( s(N), T ).
|?- from( 0, X ).
• co-Herbrand Universe: Uco(P1) = N    L where
N=[0, s(0), s(s(0)), ... ], ={ s(s(s( . . . ) ) ) }, and L is the the set
of all finite and infinite lists of elements in N,  and L.
• co-Herbrand Model:
Mco(P1)={ from(t, [t, s(t), s(s(t)), ... ]) | t  Uco(P1) }
• from(0, [0, s(0), s(s(0)), ... ])  Mco(P1) implies the query holds
• Without “coinductive” declaration of from, Mco(P1’)=
This corresponds to traditional semantics of LP with infinite trees.
Applied Logic, Programming-Languages and Systems (ALPS) Lab @ UTD Slide- 64
Descargar

Mobile Tracking Using Forward Link in Cellular Networks