Time is Not a Four-letter Word

Presentation I’ll give right now! How to add time to Declare by translating to timed LTL and timed automata.  Also how we can use this to give a priori advice concerning time, detect errors, and support planning.

Edit: There’s a slight error in the timed automaton shown; it allows going Backstage, then Getting Drunk, letting 12 hours pass, and then going to the M&G. That should not be possible, and the state s3 should be split up.

Leave a Reply

Your email address will not be published. Required fields are marked *

This site uses Akismet to reduce spam. Learn how your comment data is processed.