Towards a tableau-based procedure for PLTL based on a multi-conclusion rule and logical optimizations