Słowo czasowe

W sprawdzaniu modeli , poddziedzinie informatyki , słowo czasowe jest rozszerzeniem pojęcia słów w języku formalnym , w którym każda litera jest powiązana z dodatnim znacznikiem czasu. Sekwencja znacznika czasu musi być nie malejąca , co intuicyjnie oznacza, że ​​litery są odbierane. Na przykład system odbierający słowo przez sieć może powiązać z każdą literą czas, w którym litera została odebrana. Warunek nie malejący oznacza tutaj, że litery są odbierane we właściwej kolejności.

Język czasowy to zestaw słów czasowych.

Przykład

Rozważ windę. To, co formalnie nazywa się listem, w rzeczywistości może być informacją typu "ktoś wcisnął guzik na drugim piętrze" lub "drzwi na trzecim piętrze się otworzyły". W tym przypadku słowo czasowe to sekwencja działań podejmowanych przez windy i ich użytkowników, ze znacznikami czasu przypominającymi te działania. Słowo czasowe można następnie przeanalizować metodą formalną, aby sprawdzić, czy właściwość taka, że ​​„za każdym razem, gdy winda jest wywoływana, przyjeżdża w mniej niż trzy minuty, zakładając, że nikt nie trzymał drzwi dłużej niż piętnaście sekund”, jest zachowana. Stwierdzenie takie jak to jest zwykle wyrażane w metrycznej logice temporalnej , rozszerzenie liniowej logiki temporalnej , które pozwala wyrazić ograniczenia czasowe.

Słowo czasowe może zostać przekazane do modelu, takiego jak automat czasowy , który zadecyduje, biorąc pod uwagę litery lub działania, które już miały miejsce, jakie jest następne działanie, które należy wykonać. W naszym przykładzie, na które piętro musi jechać winda. Następnie program może przetestować ten automat czasowy i sprawdzić powyższą właściwość. Oznacza to, że spróbuje wygenerować słowo czasowe, w którym drzwi nigdy nie są otwarte dłużej niż piętnaście sekund, a użytkownik musi czekać dłużej niż trzy minuty po wezwaniu windy.

Definicja

Biorąc pod uwagę alfabet A , słowo czasowe jest sekwencją, skończoną lub nieskończoną ${\ Displaystyle w = (a_ {0}, t_ {0}) (a_ {1 }, t_ {1}) \ kropki}$ z za ${\ Displaystyle a_ {i} \ w A}$ t $\ Displaystyle t_ {i} \ w \ mathbb {R} _ {+} }$ gdzie ${\ Displaystyle t_ {i} \ równoważnik t_ {i + 1}}$ dla każdej liczby całkowitej ${\ displaystyle i}$ .

Jeśli sekwencja jest nieskończona, ale sekwencja $,$ mówi się, że czasowym , w odniesieniu do paradoksów Zenona , w których w skończonym czasie zachodzi nieskończona liczba działań.

Untimed $.$ słowo $.$ jest to $kropki}$ \ displaystyle a_ {0} a_ {1} Biorąc pod uwagę czasowy język , Untimed $L}$$displaystyle$ jest wtedy zbiorem bezczasowym $displaystyle w$ w $in L}$ .

• Alur, Rajeev; Koper, David (1994). „Teoria automatów itmed”. Informatyka teoretyczna . 126 : 190.