Abstract
Open reactive systems are systems that ideally never terminate and are intended to maintain some interaction with their environment. Temporal logic is one of the methods for formal specification description of open reactive systems. For an open reactive system specification, we do not always obtain a program satisfying it because the open reactive system program must satisfy the specification no matter how the environment of the open reactive system behaves. This problem is known as realizability and the complexity of realizability check is double or triple exponential time of the length of specification formula and realizability checking of specifications is impractical. This paper implements stepwise satisfiability checking procedure with tableau method and proof system. Stepwise satisfiability is one of the necessary conditions of realizability of reactive system specifications. The implemented procedure uses proof system that is introduced in this paper. This proof system can accelerate the decision procedure, but since it is imcomplete it cannot itself decide the realizability property of specifications. The experiment of this paper shows that the implemented procedure can decide the realizability property of several specifications.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and Unrealizable Specifications of Reactive Systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Bouyer, P., Bozzelli, L., Chevalier, F.: Controller Synthesis for MTL Specifications. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 450–464. Springer, Heidelberg (2006)
Eén, N., Mishchenko, A., Sörensson, N.: Applying Logic Synthesis for Speeding Up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 272–286. Springer, Heidelberg (2007)
Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems. NATO Advanced Summer Institutes, vol. F-13, pp. 477–498 (1985)
Kupferman, O., Madhusudan, P., Thiagarajan, P.S., Vardi, M.Y.: Open Systems in Reactive Environments: Control and Synthesis. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 92–107. Springer, Heidelberg (2000)
Ouaknine, J., Worrell, J.: On the Decidability of Metric Temporal Logic. In: Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science, pp. 188–197 (2005)
Pnueli, A., Rosner, R.: On the Synthesis of an Asynchronous Reactive Module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)
Pnueli, A., Rosner, R.: On the Synthesis of a Reactive Module. In: Proc. 16th Ann. ACM Symp. on the Principle of Programming Languages, pp. 179–190 (1989)
Mori, R., Yonezaki, Y.: Derivation of the Input Conditional Formula from a Reactive System Specification in Temporal Logic. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 567–582. Springer, Heidelberg (1994)
Emerson, E.A.: Temporal and Modal Logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. North-Holland, Amsterdam (1990)
Wolper, P.: Temporal Logic can be more expressive. Informaition and Control 56, 72–93 (1983)
Yoshiura, N.: Decision Procedures for Several Properties of Reactive System Specifications. In: Futatsugi, K., Mizoguchi, F., Yonezaki, N. (eds.) ISSS 2003. LNCS, vol. 3233, pp. 154–173. Springer, Heidelberg (2004)
The MiniSat Page, http://minisat.se/
Filiot, E., Jin, N., Raskin, J.-F.: An Antichain Algorithm for LTL Realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)
Duer-Luts, A.: LTL translation improvements in Spot. In: The 5th International Workshop on Verification and Evaluation of Computer and Communication Systems (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Neya, Y., Yoshiura, N. (2012). Stepwise Satisfiability Checking Procedure for Reactive System Specifications by Tableau Method and Proof System. In: Aoki, T., Taguchi, K. (eds) Formal Methods and Software Engineering. ICFEM 2012. Lecture Notes in Computer Science, vol 7635. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-34281-3_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-34281-3_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-34280-6
Online ISBN: 978-3-642-34281-3
eBook Packages: Computer ScienceComputer Science (R0)