Skip to Main Content
Automated Planning
book

Automated Planning

by Malik Ghallab, Dana Nau, Paolo Traverso
May 2004
Intermediate to advanced content levelIntermediate to advanced
635 pages
19h 46m
English
Morgan Kaufmann
Content preview from Automated Planning
C.3 The Model Checking Problem 563
is open. A safety requirement is that “the signal is never green when the road is
open.” Given this property as input, the model checker should return “yes.” Indeed,
there is no state of the system where the road is open and the signal is green.
We are also interested in the liveness requirements, i.e., properties that assure that
the system “works,” such as the fact that “if the signal is red, then eventually in the
future it will be green.” This corresponds to the fact that we want to allow some train
to proceed sooner or later. In this case the model checker finds a counterexample. It
is represented by the infinite sequences of states that start with red and closed, and
then have red and open forever.
Some remarks ...
Become an O’Reilly member and get unlimited access to this title plus top books and audiobooks from O’Reilly and nearly 200 top publishers, thousands of courses curated by job role, 150+ live events each month,
and much more.
Start your free trial

You might also like

Communicate with Teams More Effectively

Communicate with Teams More Effectively

Charles Humble
How to Overcome a Power Deficit

How to Overcome a Power Deficit

Cyril Bouquet, Jean-Louis Barsoux

Publisher Resources

ISBN: 9781558608566