Navegar

Colección

Datos Estadísticas

Artículo

D'Ippolito, N.; Braberman, V.; Piterman, N.; Uchitel, S. "The modal transition system control problem" (2012) 18th International Symposium on Formal Methods, FM 2012. 7436 LNCS:155-170
La versión final de este artículo es de uso interno. El editor solo permite incluir en el repositorio el artículo en su versión post-print. Por favor, si usted la posee enviela a
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Controller synthesis is a well studied problem that attempts to automatically generate an operational behaviour model of the systemto- be such that when deployed in a given domain model that behaves according to specified assumptions satisfies a given goal. A limitation of known controller synthesis techniques is that they require complete descriptions of the problem domain. This is limiting in the context of modern incremental development processes when a fully described problem domain is unavailable, undesirable or uneconomical. In this paper we study the controller synthesis problem when there is partial behaviour information about the problem domain. More specifically, we define and study the controller realisability problem for domains described as Modal Transition Systems (MTS). An MTS is a partial behaviour model that compactly represents a set of complete behaviour models in the form of Labelled Transition Systems (LTS). Given an MTS we ask if all, none or some of the LTS it describes admit an LTS controller that guarantees a given property. We show a technique that solves effectively the MTS realisability problem and is in the same complexity class as the corresponding LTS problem. © 2012 Springer-Verlag.

Registro:

Documento: Artículo
Título:The modal transition system control problem
Autor:D'Ippolito, N.; Braberman, V.; Piterman, N.; Uchitel, S.
Ciudad:Paris
Filiación:Computing Department, Imperial College London, London, United Kingdom
Departamento de Computatión, FCEyN, Universidad de Buenos Aires, Argentina
Department of Computer Science, University of Leicester, Leicester, United Kingdom
Palabras clave:Behaviour models; Complexity class; Controller synthesis; Domain model; Incremental development; Labelled transition systems; Modal Transition Systems; Problem domain; Realisability; Artificial intelligence; Controllers
Año:2012
Volumen:7436 LNCS
Página de inicio:155
Página de fin:170
DOI: http://dx.doi.org/10.1007/978-3-642-32759-9_15
Título revista:18th International Symposium on Formal Methods, FM 2012
Título revista abreviado:Lect. Notes Comput. Sci.
ISSN:03029743
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7436LNCS_n_p155_DIppolito

Referencias:

  • Asarin, E., Maler, O., Pnueli, A., Sifakis, J., Controller synthesis for timed automata (1998) SSC
  • Bertolino, A., Inverardi, P., Pelliccione, P., Tivoli, M., Automatic synthesis of behavior protocols for composable web-services (2009) FSE, , ACM
  • Bruns, G., Godefroid, P., Model Checking Partial State Spaces with 3-Valued Temporal Logics (1999) LNCS, 1633, pp. 274-287. , Halbwachs, N., Peled, D.A. (eds.) CAV 1999. Springer, Heidelberg
  • Bruns, G., Godefroid, P., Generalized Model Checking: Reasoning about Partial State Spaces (2000) LNCS, 1877, pp. 168-182. , Palamidessi, C. (ed.) CONCUR 2000. Springer, Heidelberg
  • Dalpiaz, F., Giorgini, P., Mylopoulos, J., An Architecture for Requirements-Driven Self-reconfiguration (2009) LNCS, 5565, pp. 246-260. , van Eck, P., Gordijn, J., Wieringa, R. (eds.) CAiSE 2009. Springer, Heidelberg
  • Damas, C., Lambeau, B., Van Lamsweerde, A., Scenarios, goals, and state machines: A win-win partnership for model synthesis (2006) FSE, , ACM
  • D'Ippolito, N., http://www.doc.ic.ac.uk/-srdipi/techfm2012, Technical Report; D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesising nonanomalous event-based controllers for liveness goals ACM TOSEM, 22 (1). , to appear 2013
  • D'Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S., Synthesis of live behaviour models for fallible domains (2011) ICSE, , ACM
  • D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S., Mtsa: The modal transition system analyser (2008) ASE, , IEEE
  • Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) FSE, , ACM
  • Godefroid, P., Piterman, N., LTL Generalized Model Checking Revisited (2009) LNCS, 5403, pp. 89-104. , Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. Springer, Heidelberg
  • Henzinger, T.A., Jhala, R., Majumdar, R., Counterexample-Guided Control (2003) LNCS, 2719, pp. 886-902. , Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J., et al. (eds.) ICALP 2003. Springer, Heidelberg
  • Inverardi, P., Tivoli, M., A reuse-based approach to the correct and automatic composition of web-services (2007) ESSPE, , ACM
  • Jackson, M., The world and the machine (1995) ICSE, , ACM
  • Kazhamiakin, R., Pistore, M., Roveri, M., Formal verification of requirements using spin: A case study on web services (2004) SEFM, , IEEE
  • Keller, R.M., Formal verification of parallel programs (1976) CACM 19
  • Van Lamsweerde, A., (2009) Requirements Engineering - From System Goals to UML Models to Software Specifications, , Wiley
  • Larsen, K., Thomsen, B., A Modal Process Logic (1988) LICS, , IEEE
  • Larsen, K.G., Xinxin, L., Equation solving using modal transition systems (1990) LICS, , IEEE
  • Letier, E., Van Lamsweerde, A., Agent-based tactics for goal-oriented requirements elaboration (2002) ICSE, , ACM
  • Piterman, N., Pnueli, A., Sa'ar, Y., Synthesis of Reactive(1) Designs (2005) LNCS, 3855, pp. 364-380. , Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. Springer, Heidelberg
  • Pnueli, A., The temporal logic of programs (1977) FOCS, , IEEE
  • Pnueli, A., Rosner, R., On the synthesis of a reactive module (1989) POPL, , ACM
  • Raskin, J.F., Chatterjee, K., Doyen, L., Henzinger, T.A., Algorithms for omega-regular games with imperfect information (2007) LMCS, 3 (3)
  • Sykes, D., Heaven, W., Magee, J., Kramer, J., Plan-directed architectural change for autonomous systems (2007) SAVCBS
  • Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) TOSEM, 35A4 - Digiteo; AdaCore; SNCF; LEI; ENSTA ParisTech

Citas:

---------- APA ----------
D'Ippolito, N., Braberman, V., Piterman, N. & Uchitel, S. (2012) . The modal transition system control problem. 18th International Symposium on Formal Methods, FM 2012, 7436 LNCS, 155-170.
http://dx.doi.org/10.1007/978-3-642-32759-9_15
---------- CHICAGO ----------
D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S. "The modal transition system control problem" . 18th International Symposium on Formal Methods, FM 2012 7436 LNCS (2012) : 155-170.
http://dx.doi.org/10.1007/978-3-642-32759-9_15
---------- MLA ----------
D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S. "The modal transition system control problem" . 18th International Symposium on Formal Methods, FM 2012, vol. 7436 LNCS, 2012, pp. 155-170.
http://dx.doi.org/10.1007/978-3-642-32759-9_15
---------- VANCOUVER ----------
D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S. The modal transition system control problem. Lect. Notes Comput. Sci. 2012;7436 LNCS:155-170.
http://dx.doi.org/10.1007/978-3-642-32759-9_15