Hourglass Systems

In this paper, we first describe a simplified scenario observed in mining operations, where trucks are loaded and emptied at different locations. We will then look at ways that we can model this subsystem using timed automata so we may be able to apply model checking techniques on such systems. Specifically, we will look at modifications to the Hourglass Automata and Interrupt Timed Automata to model the truck loading, unloading scenario, and we will show that reachability is maintained.

• Type: Journal
• Year: 2015
• Where: ACSC
• Authors: Yuki Osada, Mark Reynolds, Tim French
• Keywords: ACSC 2015, Theoretical Computer Science