Clock (model checking) (original) (raw)
In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measures how much time passed since a particular event occurs, in this sense, a clock is more precisely an abstraction of a stopwatch. In a model of some particular program, the value of the clock may either be the time since the program was started, or the time since a particular event occurred in the program. Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and . They are also used in programs such as UPPAAL which implement timed automata.
| Property | Value |
|---|---|
| dbo:abstract | In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measures how much time passed since a particular event occurs, in this sense, a clock is more precisely an abstraction of a stopwatch. In a model of some particular program, the value of the clock may either be the time since the program was started, or the time since a particular event occurred in the program. Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and . They are also used in programs such as UPPAAL which implement timed automata. Generally, the model of a system uses many clocks. Those multiple clocks are required in order to track a bounded number of events. All of those clocks are synchronized. That means that the difference in value between two fixed clocks is constant until one of them is restarted. In the language of electronics, it means that clock's jitter is null. (en) |
| dbo:wikiPageID | 60280819 (xsd:integer) |
| dbo:wikiPageLength | 9212 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1052322289 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Timed_propositional_temporal_logic dbr:Model_checking dbr:Logical_conjunction dbr:Computer_science dbr:First-order_logic dbr:Difference_bound_matrix dbr:Region_(model_checking) dbr:Jitter dbc:Automata_(computation) dbc:Model_checking dbr:Zone_(convex_polytope) dbr:Signal_automaton dbr:Stopwatch dbr:Timed_automaton dbr:UPPAAL dbr:Clock_temporal_logic |
| dbp:wikiPageUsesTemplate | dbt:R |
| dcterms:subject | dbc:Automata_(computation) dbc:Model_checking |
| rdfs:comment | In model checking, a subfield of computer science, a clock is a mathematical object used to model time. More precisely, a clock measures how much time passed since a particular event occurs, in this sense, a clock is more precisely an abstraction of a stopwatch. In a model of some particular program, the value of the clock may either be the time since the program was started, or the time since a particular event occurred in the program. Those clocks are used in the definition of timed automaton, signal automaton, timed propositional temporal logic and . They are also used in programs such as UPPAAL which implement timed automata. (en) |
| rdfs:label | Clock (model checking) (en) |
| owl:sameAs | wikidata:Clock (model checking) https://global.dbpedia.org/id/AR3g2 |
| prov:wasDerivedFrom | wikipedia-en:Clock_(model_checking)?oldid=1052322289&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Clock_(model_checking) |
| is dbo:wikiPageWikiLink of | dbr:Timed_propositional_temporal_logic dbr:Alternating_timed_automaton dbr:Difference_bound_matrix dbr:Region_(model_checking) dbr:Signal_automaton dbr:Timed_automaton |
| is foaf:primaryTopic of | wikipedia-en:Clock_(model_checking) |