tijdslogica

Tijdslogica is een tak van logica die tijd en temporele relaties tussen gebeurtenissen formaliseert. Het biedt formele middelen om uitspraken te doen over hoe toestanden in de loop der tijd veranderen en hoe gebeurtenissen met elkaar in verband staan. Modellen voor tijdslogica bestaan meestal uit toestanden en overgangen tussen toestanden, vaak voorgesteld als Kripke-structuren of als oneindige tijdlijnen. Proposities kunnen waar of onwaar zijn in een gegeven toestand, en temporele operatoren tonen aan wat er op toekomstige momenten geldt.

Er zijn verschillende families van tijdslogica. Lineaire tijdlogica (LTL) beschouwt één tijdlijn tegelijk en maakt gebruik van operatoren zoals X (volgende), F (uiteindelijk), G (altijd) en U (totdat). Branching-time logica, zoals CTL en CTL*, verwerkt verschillende mogelijke toekomstpaden en combineert padquantifiers als A (alle paden) en E (een pad bestaat) met temporele operatoren. First-order temporele logica voegt daarnaast quantificatie over individuen toe, waardoor rijkere eigenschappen kunnen worden geformuleerd.

Semantiek in tijdslogica is meestal gebaseerd op evaluatie langs tijdlijnen (bij LTL) of op boomachtige structuren waarin meerdere toekomstpaden mogelijk zijn (bij CTL/CTL*). Deze logica is bijzonder relevant voor formele verificatie en model checking: het automatisch verifiëren van correcte werking van software, hardware en gedistribueerde systemen, zeker waar tijdsvoorwaarden een rol spelen.

Andere varianten bestrijken real-time aspecten met timingbeperkingen, probabilistische temporele logica voor stochasticiteit en logica die tijd en kennis combineert. Tijdslogica blijft een centraal gereedschap in de formele specificatie en verificatie van tijdafhankelijke systemen.