Linear temporal logic and Linear Dynamic Logic on finite traces