On Designated Values in Multi-Valued CTLS* Model Checking

• Autorzy: Konikowska B. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

A multi-valued version of CTLS* (mv-CTLS*), where both the propositions and the accessibility relation are multi-valued, taking values in a complete lattice with a complement, is considered. Contrary to all the existing model checking results for multi-valued modal logics, our lattices are not required to be finite. A set of restrictions is provided under which there is a direct translation from mv-CTLS* to CTLS* model checking problem for designated values. Bisimulation induced by mv-CTLS* is characterized.

Słowa kluczowe

EN

multivalued logic; syntax of mv-CTL*; semantics of mv-CTL*; bisimulation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2004
• Tom: Vol. 60, nr 1-4
• Strony: 211--224
• Opis fizyczny: Bibliogr. 22 poz.

Twórcy

autor

Konikowska B.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland

autor

Penczek W.

• Institute of Computer Science, Polish Academy of Science, Ordona 21, 01-237 Warsaw, Poland

Bibliografia

• [BCG88] M. C. Browne, E. M. Clarke, and O. Grumberg, Characterizing finite Kripke structures in propositional temporal logic, Theoretical Computer Science 59( 1/2) (1988), pp. 115-131.
• [Bel78] N. Belnap. A useful four-valued logic, Modern Uses of Multiple-Valued Logics (J. Dunn and G. Epstein, eds.), Reidel Publishing Comp., 1978, pp. 8-37.
• [BG99] G. Bruns and P. Godefroid. Model checking partial state spaces. Proc. of the 11 th Int. Conf. on Computer Aided Verification (CAV’99), LNCS, vol. 1633, Springer-Verlag, 1999, pp. 274-287.
• [BG00] G. Bruns and P. Godefroid, Generalized model checking: Reasoning about partial state spaces, Proc. of the 11 th Int. Conf. on Concurrency Theory (CONCUR'OO). LNCS, vol. 1877, Springer-Verlag, 2000, pp. 168-182.
• [BG03] G. Bruns and P. Godefroid. Model checking with multi-valued logics. Bell Labs Technical Memorandum ITD-03-44535H. May 2003.
• [CEPO1] M. Chechik. S. Easterbrook. and V. Petrovykh, Model checking over multi-valued logics. Proc. ot the Int. Symp. Formal Methods Europe (FME'01). LNCS, vol. 2021, Springer-Verlag, 2001. pp. 72-98.
• [CGP99] E. M. Clarke, O. Grumberg, and D. Peled. Model checking. MIT Press. 1999.
• [CheOO] M. Chechik, On interpreting results of model-checking with abstraction, Tech. Report CSRG 417. University of Toronto, Toronto M5S 3G4, Canada, 2000.
• [CM03] M. Chechik and W. MacCaull, CTL model-checking over logics with non-classical negations. Proc. of the 33rd IEEE Int. Symp. on Multi-Valued Logics (ISMVL4)3), IEEE Comp. Soc. Press, May 2003, pp. 293-300.
• [DGD94] D. Dams, R. Gerth. G. Dohmen. R. Herrmann. P. Kelb, and H. Pargmann. Model checking using adaptive state and data abstraction. Proc. of the 6th Int. Conf. on Computer Aided Verification (CAV'94). LNCS. vol. 818, Springer-Verlag, 1994. pp. 455-467.
• [DM02] A. Dańko and G. Mirkowska, Muliti-valued boolean-fuzzy logics, Proc. of the Int. Workshop on Concurrency. Specification and Programming (CS&P'02) (H.-D. Burhard et al., ed.), 2002, pp. 101-104.
• [EC01] S. Easterbrook and M. Chechik, A framework for multi-valued reasoning over inconsistent viewpoints, Proc. of the 23rd Int. Conf. on Software Engineering (ICSE'01). IEEE Comp. Soc. Press, 2001, pp. 411-420.
• [Fit91] M. Fitting, Many-valued modal logics, Fundamenta Informaticae 15(3-4) (1991). pp. 335-350.
• [Fit92] M. Fitting, Many-valued modal logics II. Fundamenta Informaticae 17 (1992). pp. 55-73.
• [GC03] A. Gurfinkel and M. Chechik, Multi-valued model-checking via classical model checking, Concur’03. LNCS. vol. 2761, Springer-Verlag, 2003, pp. 265-279.
• [Göd86] К. Gödel, On the intuitionistisc propositional calculus, 1933, Kurt Gödel: Collected Works (S. Feferman, J. Dawson. S. Kleene, G. Moore. R. Solovay. and J. van Heijenoort, eds.), vol. 1: Publications 1929-1936. Oxford University Press, 1986.
• [Haj98] P. Hajek, Metamathematics of fuzzy logic, Kluwer Academic Publishers, 1998.
• [Kle52] S. C. Kleene. Introduction to metamathematics, North-Holland, 1952.
• [KP02] B. Konikowska and W. Penczek. Reducing model checking from multi-valued CTL* to CTL*. Proc. of the 13th Int. Conf. on Concurrency Theory (CONCUR'(02). LNCS, vol. 2421, Springer-Verlag. 2002, pp. 226-239.
• [KP03] B. Konikowska and W. Penczek. Model checking for multi-valued computation tree logics, Beyond Two: Theory and Applications of Multiple Valued Logic (M. Fitting and E. Orłowska, eds.), Physica-Verlag, 2003, pp. 193-210.
• [PWZ02] W. Penczek. B. Woźna, and A. Zbrzezny. Bounded model checking for the universal fragment of CTL, Fundamenta Informaticae 51(1-2) (2002). pp. 135-156.
• [RT52] J. B. Rosser and A. R. Turquette. Many-valued logics, North-Holland. 1952.