A model checker for linear time temporal logic
Copyright policy )A model checker for linear time temporal logic
Abstract This report describes the design and implementation of a model checker for linear time temporal logic. The model checker uses a depth-first search algorithm that attempts to find a minimal satisfying model and uses as little space as possible during the checking procedure. The depth-first nature of the algorithm enables the model checker to be used where space is at a premium.
- University of Salford United Kingdom
- Temple Group (United Kingdom) United Kingdom
program verification, Model checking, Logic in computer science, Specification and verification (program logics, model checking, etc.), temporal logic, Program verification, Temporal logic, Modal logic (including the logic of norms), model checking
program verification, Model checking, Logic in computer science, Specification and verification (program logics, model checking, etc.), temporal logic, Program verification, Temporal logic, Modal logic (including the logic of norms), model checking
citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).2 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Average impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Average
Citations provided by BIP!Popularity provided by BIP!