28 lines
872 B
Markdown
28 lines
872 B
Markdown
---
|
|
id: 20260109155415
|
|
title: Timed Automata
|
|
type: permanent
|
|
created: 2026-01-09T20:54:15Z
|
|
modified: 2026-01-09T21:13:51Z
|
|
tags: []
|
|
---
|
|
|
|
# Timed Automata
|
|
Timed automata are linear hybrid automata with the
|
|
special condition that every continuously changing variable
|
|
is a *clock*. That means that every variable varies one to
|
|
one with time, just counting time.
|
|
|
|
Timed automata have invariants and guards that compare time
|
|
only with constants. There are no other continuous dynamics
|
|
here.
|
|
|
|
An example of a timed automata is something like an alarm.
|
|
Easy peasy, is time greater or less than a value. If it is,
|
|
trigger the alarm! One might also have a constant setting
|
|
whether or not an alarm is 'enabled'. But, there's no other
|
|
dynamics than time itself.
|
|
|
|
## Relevant Sources
|
|
[[hybrid-automata-an-algorithmic-approach-to-the-specification-and-verification-of-hybrid-systems]]
|