Loading...
Please wait, while we are loading the content...
Similar Documents
Differential Invariants and Symbolic Integration for Distributed Hybrid Systems (CMU-CS-12-107)
| Content Provider | Semantic Scholar |
|---|---|
| Author | Renshaw, David W. Platzer, André |
| Copyright Year | 2012 |
| Abstract | We present a formal proof of collision avoidance for a simple distributed hybrid system consisting of an arbitrary finite number of cars on a one dimensional road. Our cars take actions independently from one another and without synchronization, thus behaving in a truly distributed manner. We allow cars to enter and exit the road. For the continuous dynamics, we show how differential invariants and symbolic solutions can be used together harmoniously to prove things that neither could prove alone. We have fully mechanized our formal proof within our theorem prover KeYmaeraD. |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | http://reports-archive.adm.cs.cmu.edu/anon/2012/CMU-CS-12-107.pdf |
| Alternate Webpage(s) | http://repository.cmu.edu/cgi/viewcontent.cgi?article=3737&context=compsci |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~dwrensha/papers/disi.pdf |
| Alternate Webpage(s) | http://www.cs.cmu.edu/~renshaw/papers/disi.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
