Automated Program Synthesis and Application in Game Programming
S
o
f
t
w
a
r
e
S
y
n
t
h
e
s
i
s
Participants: Omri Ajchenbaum and Daniel Hasson
Supervised by Dr. Hillel Kugler
Mid-Project presentations: February 2016
W
h
a
t
i
s
S
y
n
t
h
e
s
i
s
?
“Program synthesis is a special form of automatic programming that is most
often paired with a technique for formal verification. The goal is to construct
automatically a program that provably satisfies a given high-level
specification. In contrast to other automatic programming techniques, the
specifications are usually non-algorithmic statements of an
appropriate logical calculus.”
Wikipedia
“Given a requirement which a circuit is to satisfy, we may suppose the
requirement expressed in some suitable logistic system … The synthesis
problem is then to find recursion equivalences representing a circuit that
satisfies the given requirement (or alternatively, to determine that there is
no such circuit).
A. Church (1957)
C
o
m
p
u
t
a
t
i
o
n
T
r
e
e
L
o
g
i
c
(
C
T
L
)
•
CTL is a type of temporal logic. Temporal Logic was introduced by Pnueli (1977) to
specify temporal behavior of reactive systems.
•
In CTL one can express properties that should hold for all the paths that start in a
state, as well as for properties that should hold just for some of the paths.
•
For instance CTL formula AF p - expresses the condition that, for all the paths (A)
starting from a given state, eventually in the future condition p must hold.
•
CTL formula EF p, on the other hand, requires that there exists some path (E) that
eventually in the future satisfies p.
•
A tool and language that implements CTL model-checking - NuSMV
E
x
a
m
p
l
e
–
T
i
c
T
a
c
T
o
e
g
a
m
e
In a tic-tac-toe game one must arrange 3 consecutive symbols in a 3X3 square board.
Problem specifications:
•
A player must use only use his symbol, play only on his turn and only mark an empty
square.
We started by adding a no-lose specification with the following CTL formula:
!(EX(AX(EX(AX(EX(AX(EX(AX(EX !OtherPlayerWin)))))))))
We used this specification because we wanted NuSMV to return a counter example which
ensures the 2
nd
player does not win.
We then created a program using CPP which governs the board state, turn state and gives
us a simple GUI. The CPP creates a new NuSMV code for each turn in order to implement
all the specifications, then processes and “plays” according to the NuSMV result.
At the next stage we added, by using CTL, the specification for win-first-if-possible strategy:
!(EX(AX(EX(AX(EX(AX(EX(AX(EX win1)))))))))
W
h
a
t
’
s
n
e
x
t
?
C
a
r
-
t
o
-
X
c
o
m
m
u
n
i
c
a
t
i
o
n
T
h
e
p
r
o
b
l
e
m
:
C
a
r
s
a
r
e
d
r
i
v
i
n
g
o
n
a
t
w
o
-
l
a
n
e
r
o
a
d
.
O
n
o
n
e
o
f
t
h
e
l
a
n
e
s
t
h
e
r
e
’
s
a
n
o
b
s
t
a
c
l
e
w
h
i
c
h
b
l
o
c
k
s
p
a
r
t
o
f
i
t
.
W
e
w
a
n
t
t
o
s
y
n
t
h
e
s
i
z
e
a
d
r
i
v
e
r
a
s
s
i
s
t
a
n
c
e
s
y
s
t
e
m
w
h
i
c
h
t
e
l
l
s
t
h
e
d
r
i
v
e
r
i
f
t
h
e
o
t
h
e
r
l
a
n
e
i
s
f
r
e
e
a
n
d
h
e
c
a
n
b
y
p
a
s
s
t
h
e
o
b
s
t
a
c
l
e
.
H
o
w
c
a
n
w
e
a
c
h
i
e
v
e
t
h
a
t
?
S
y
s
t
e
m
r
u
l
e
s
a
n
d
s
p
e
c
i
f
i
c
a
t
i
o
n
•
Collect/Transmit relevant information about cars and traffic in real time.
•
Ensure no “crashes” occur (robust solution).
•
Ensure “safety” and “liveness” of system.
•
Enable scaling of the system to allow large number of cars (we shall start with up to 4).
•
Ensure car does not wait more then K time units.
Next Steps:
- Implement Synthesis method using NuSMV framework (open source)
- Evaluate compared to state of the art methods (Synthesis Competitions)
- In future may be tested in real robotic system (Collaboration with Greenyer at Hannover,
A. Marron at Weizmann Institute)
Exploring program synthesis as a method for automatic program construction to meet high-level specifications, focusing on applications in game programming. Discusses concepts like Church Synthesis, Computation Tree Logic (CTL), and real-life examples like Tic-Tac-Toe game strategy synthesis. Explores potential future applications in Car-to-X communication for driver assistance systems.
Uploaded on Sep 22, 2024 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Software Synthesis Participants: Omri Ajchenbaum and Daniel Hasson Supervised by Dr. Hillel Kugler Mid-Project presentations: February 2016
What is Synthesis? Program synthesis is a special form of automatic programming that is most often paired with a technique for formal verification. The goal is to construct automatically a program that provably satisfies a given high-level specification. In contrast to other automatic programming techniques, the specifications are usually non-algorithmic statements of an appropriate logical calculus. Wikipedia Given a requirement which a circuit is to satisfy, we may suppose the requirement expressed in some suitable logistic system The synthesis problem is then to find recursion equivalences representing a circuit that satisfies the given requirement (or alternatively, to determine that there is no such circuit). A. Church (1957)
Computation Tree Logic (CTL) CTL is a type of temporal logic. Temporal Logic was introduced by Pnueli (1977) to specify temporal behavior of reactive systems. In CTL one can express properties that should hold for all the paths that start in a state, as well as for properties that should hold just for some of the paths. For instance CTL formula AF p - expresses the condition that, for all the paths (A) starting from a given state, eventually in the future condition p must hold. CTL formula EF p, on the other hand, requires that there exists some path (E) that eventually in the future satisfies p. A tool and language that implements CTL model-checking - NuSMV
Example Tic Tac Toe game In a tic-tac-toe game one must arrange 3 consecutive symbols in a 3X3 square board. Problem specifications: A player must use only use his symbol, play only on his turn and only mark an empty square. We started by adding a no-lose specification with the following CTL formula: !(EX(AX(EX(AX(EX(AX(EX(AX(EX !OtherPlayerWin))))))))) We used this specification because we wanted NuSMV to return a counter example which ensures the 2ndplayer does not win. We then created a program using CPP which governs the board state, turn state and gives us a simple GUI. The CPP creates a new NuSMV code for each turn in order to implement all the specifications, then processes and plays according to the NuSMV result. At the next stage we added, by using CTL, the specification for win-first-if-possible strategy: !(EX(AX(EX(AX(EX(AX(EX(AX(EX win1)))))))))
Car-to-X communication The problem: Cars are driving on a two-lane road. On one of the lanes there s an obstacle which blocks part of it. We want to synthesize a driver assistance system which tells the driver if the other lane is free and he can bypass the obstacle. How can we achieve that?
System rules and specification Collect/Transmit relevant information about cars and traffic in real time. Ensure no crashes occur (robust solution). Ensure safety and liveness of system. Enable scaling of the system to allow large number of cars (we shall start with up to 4). Ensure car does not wait more then K time units. Next Steps: - Implement Synthesis method using NuSMV framework (open source) - Evaluate compared to state of the art methods (Synthesis Competitions) - In future may be tested in real robotic system (Collaboration with Greenyer at Hannover, A. Marron at Weizmann Institute)
