Verifying Memoryless Sequential Decision-making of Large Language Models