CourseWare Wiki
Search
Log In
old
courses
a4m33au
term_en
Warning
This page is located in archive.
Differences
This shows you the differences between two versions of the page.
View differences:
Side by Side
Inline
Go
Link to this comparison view
Both sides previous revision
Previous revision
2014/04/17 00:54 vyskoji1 File moved, media files copied and media links repaired
2014/04/17 00:52 vyskoji1 File moved, media files copied and media links repaired
2014/04/17 00:46 vyskoji1 [Timed Automata Variant]
2014/04/01 21:12 jakubja5 [Technical Notes]
2014/04/01 21:11 jakubja5 [Technical Notes]
2014/04/01 21:10 jakubja5 [Technické poznámky]
2014/04/01 21:09 jakubja5 [Automated Reasoning Version]
2014/04/01 21:08 jakubja5 [Timed Automata Variant]
2014/04/01 21:02 jakubja5 [Varianta pomocí časových automatů]
2014/04/01 20:58 jakubja5 [Technical Notes]
2014/04/01 20:58 jakubja5 [Technické poznámky]
2014/04/01 20:53 jakubja5 [Automated Reasoning Version]
2014/04/01 16:56 jakubja5 [Railway Station Critical Situations]
2014/04/01 16:55 jakubja5 [Varianta automatické dokazování]
2014/04/01 16:51 jakubja5 [Data Formats]
2014/04/01 16:51 jakubja5 [Data Formats]
2014/04/01 16:49 jakubja5 [Data Formats]
2014/04/01 16:48 jakubja5 [Datové formáty]
2014/04/01 16:48 jakubja5 [Term Assignment - Railway Station]
2014/04/01 16:42 jakubja5 [Assignments]
2014/04/01 14:26 jakubja5 [Úkoly]
2014/04/01 14:22 jakubja5 [Railway Station Critical States]
2014/04/01 14:20 jakubja5 [Kritické stavy v nádraží]
2014/04/01 13:42 jakubja5 [Railway Station Properties]
2014/04/01 13:37 jakubja5
2014/04/01 13:23 jakubja5
2014/04/01 13:10 jakubja5
2014/04/01 13:05 jakubja5
2014/04/01 13:04 jakubja5
2014/04/01 13:03 jakubja5 created
Go
Next revision
Previous revision
2014/04/17 00:54 vyskoji1 File moved, media files copied and media links repaired
2014/04/17 00:52 vyskoji1 File moved, media files copied and media links repaired
2014/04/17 00:46 vyskoji1 [Timed Automata Variant]
2014/04/01 21:12 jakubja5 [Technical Notes]
2014/04/01 21:11 jakubja5 [Technical Notes]
2014/04/01 21:10 jakubja5 [Technické poznámky]
2014/04/01 21:09 jakubja5 [Automated Reasoning Version]
2014/04/01 21:08 jakubja5 [Timed Automata Variant]
2014/04/01 21:02 jakubja5 [Varianta pomocí časových automatů]
2014/04/01 20:58 jakubja5 [Technical Notes]
2014/04/01 20:58 jakubja5 [Technické poznámky]
2014/04/01 20:53 jakubja5 [Automated Reasoning Version]
2014/04/01 16:56 jakubja5 [Railway Station Critical Situations]
2014/04/01 16:55 jakubja5 [Varianta automatické dokazování]
2014/04/01 16:51 jakubja5 [Data Formats]
2014/04/01 16:51 jakubja5 [Data Formats]
2014/04/01 16:49 jakubja5 [Data Formats]
2014/04/01 16:48 jakubja5 [Datové formáty]
2014/04/01 16:48 jakubja5 [Term Assignment - Railway Station]
2014/04/01 16:42 jakubja5 [Assignments]
2014/04/01 14:26 jakubja5 [Úkoly]
2014/04/01 14:22 jakubja5 [Railway Station Critical States]
2014/04/01 14:20 jakubja5 [Kritické stavy v nádraží]
2014/04/01 13:42 jakubja5 [Railway Station Properties]
2014/04/01 13:37 jakubja5
2014/04/01 13:23 jakubja5
2014/04/01 13:10 jakubja5
2014/04/01 13:05 jakubja5
2014/04/01 13:04 jakubja5
2014/04/01 13:03 jakubja5 created
Go
Next revision
Both sides next revision
courses:a4m33au:term_en [2014/04/01 21:08]
jakubja5
[Timed Automata Variant]
courses:a4m33au:term_en [2014/04/17 00:46]
vyskoji1
[Timed Automata Variant]
Line 68:
Line 68:
- Railway station formalization:
- Railway station formalization:
- Formalize in the First Order Logic in the TPTP language the "physical" railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions. Every time dependent predicate //p// that describe something that we are able to establish has to be described by at most one formula of the shape //p(T+1) <=> φ// where formula //φ// depends only conditions in time //T// or antecedent (this syntactically guaranties correctness of the definition). This covers the state of switches, position of trains, and so on. This does not cover the engine driver will which we do not know (we know only that every train departs at some time).
- Formalize in the First Order Logic in the TPTP language the "physical" railway station behavior, that is, how trains go through the railway station based on the state of signaling devices and engine driver decisions. Every time dependent predicate //p// that describe something that we are able to establish has to be described by at most one formula of the shape //p(T+1) <=> φ// where formula //φ// depends only conditions in time //T// or antecedent (this syntactically guaranties correctness of the definition). This covers the state of switches, position of trains, and so on. This does not cover the engine driver will which we do not know (we know only that every train departs at some time).
-
-
Show
that this formalization is not contradictory with additional conditions which
describe
that a train
departs
from
a
node to another
+
-
Prove
that this formalization is not contradictory with additional conditions which
say
that a train
moves
from
one
node to another
as soon as possible (that is, the engine driver decides to depart immediately).
- Formalize the railway station control system in the same way as in point 1.
- Formalize the railway station control system in the same way as in point 1.
- Prove that the formalization of the railway station together with the control system is not contradictory.
- Prove that the formalization of the railway station together with the control system is not contradictory.
Line 77:
Line 78:
- The output of your program will be //commented// files in the TPTP language together with the output of a selected theorem prover or a model checker.
- The output of your program will be //commented// files in the TPTP language together with the output of a selected theorem prover or a model checker.
- Use heavily the TPTP directive [[http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#include|include]] to keep TPTP files readable and without duplicity.
- Use heavily the TPTP directive [[http://www.cs.miami.edu/~tptp/TPTP/SyntaxBNF.html#include|include]] to keep TPTP files readable and without duplicity.
-
-
You
program must be executable in a computer lab without additional SW (except the theorem prover or model checker).
+
-
Your
program must be executable in a computer lab without additional SW (except the theorem prover or model checker)
. Otherwise you will need to present your solution on your computer
.
-
===== Timed Automata
Variant
=====
+
===== Timed Automata
Version
=====
A railway station can be modeled both in discrete or in continues time. The control system determines the state of switches and signaling devices at every time moment.
A railway station can be modeled both in discrete or in continues time. The control system determines the state of switches and signaling devices at every time moment.
Line 94:
Line 95:
-
====
Technické poznámky
====
+
====
Technical Notes
====
-
-
Výstup programu budou soubory ve formátu
XML
pro zpracovaní systémem
UPPALL
a UPPALLem zpracované výsledky dotazů dokazující požadované vlastnosti řešení
.
+
-
The output of your program should be in
XML
format acceptable by the
UPPALL
system and the output of the UPPALL system which proves required properties
.
-
-
Řešení by mělo být spustitelné v počítačové laboratoři bez instalace dodatečného
SW.
V opačném případě budete muset svoje řešení předvést na vlastním počítači
.
+
-
Your program must be executable in a computer lab without additional
SW.
Otherwise you will need to present your solution on your computer
.
courses/a4m33au/term_en.txt
· Last modified: 2014/04/17 00:54 by
vyskoji1