The modal transition system control problem

Mostrar otras versiones (1)

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...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: D'Ippolito, N.
Otros Autores: Braberman, V., Piterman, N., Uchitel, S.
Formato: Acta de conferencia Capítulo de libro
Lenguaje:Inglés
Publicado: 2012
Acceso en línea:Registro en Scopus
DOI
Handle
Registro en la Biblioteca Digital
Aporte de:Registro referencial: Solicitar el recurso aquí
Biblioteca Central Dr. Luis F. Leloir (FCEN) de Universidad de Buenos Aires
LEADER 07567caa a22008057a 4500
001 PAPER-9329
003 AR-BaUEN
005 20230518203914.0
008 190411s2012 xx ||||fo|||| 00| 0 eng|d
024 7 |2 scopus  |a 2-s2.0-84865995885 
040 |a Scopus  |b spa  |c AR-BaUEN  |d AR-BaUEN 
100 1 |a D'Ippolito, N. 
245 1 4 |a The modal transition system control problem 
260 |c 2012 
270 1 0 |m D'Ippolito, N.; Computing Department, Imperial College London, London, United Kingdom 
506 |2 openaire  |e Política editorial 
504 |a Asarin, E., Maler, O., Pnueli, A., Sifakis, J., Controller synthesis for timed automata (1998) SSC 
504 |a Bertolino, A., Inverardi, P., Pelliccione, P., Tivoli, M., Automatic synthesis of behavior protocols for composable web-services (2009) FSE, , ACM 
504 |a 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 
504 |a 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 
504 |a 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 
504 |a Damas, C., Lambeau, B., Van Lamsweerde, A., Scenarios, goals, and state machines: A win-win partnership for model synthesis (2006) FSE, , ACM 
504 |a 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 
504 |a D'Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S., Synthesis of live behaviour models for fallible domains (2011) ICSE, , ACM 
504 |a D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S., Mtsa: The modal transition system analyser (2008) ASE, , IEEE 
504 |a Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) FSE, , ACM 
504 |a 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 
504 |a 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 
504 |a Inverardi, P., Tivoli, M., A reuse-based approach to the correct and automatic composition of web-services (2007) ESSPE, , ACM 
504 |a Jackson, M., The world and the machine (1995) ICSE, , ACM 
504 |a Kazhamiakin, R., Pistore, M., Roveri, M., Formal verification of requirements using spin: A case study on web services (2004) SEFM, , IEEE 
504 |a Keller, R.M., Formal verification of parallel programs (1976) CACM 19 
504 |a Van Lamsweerde, A., (2009) Requirements Engineering - From System Goals to UML Models to Software Specifications, , Wiley 
504 |a Larsen, K., Thomsen, B., A Modal Process Logic (1988) LICS, , IEEE 
504 |a Larsen, K.G., Xinxin, L., Equation solving using modal transition systems (1990) LICS, , IEEE 
504 |a Letier, E., Van Lamsweerde, A., Agent-based tactics for goal-oriented requirements elaboration (2002) ICSE, , ACM 
504 |a 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 
504 |a Pnueli, A., The temporal logic of programs (1977) FOCS, , IEEE 
504 |a Pnueli, A., Rosner, R., On the synthesis of a reactive module (1989) POPL, , ACM 
504 |a Raskin, J.F., Chatterjee, K., Doyen, L., Henzinger, T.A., Algorithms for omega-regular games with imperfect information (2007) LMCS, 3 (3) 
504 |a Sykes, D., Heaven, W., Magee, J., Kramer, J., Plan-directed architectural change for autonomous systems (2007) SAVCBS 
504 |a Uchitel, S., Brunet, G., Chechik, M., Synthesis of partial behavior models from properties and scenarios (2009) TOSEM, 35A4 - Digiteo; AdaCore; SNCF; LEI; ENSTA ParisTech 
520 3 |a 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.  |l eng 
593 |a Computing Department, Imperial College London, London, United Kingdom 
593 |a Departamento de Computatión, FCEyN, Universidad de Buenos Aires, Argentina 
593 |a Department of Computer Science, University of Leicester, Leicester, United Kingdom 
690 1 0 |a BEHAVIOUR MODELS 
690 1 0 |a COMPLEXITY CLASS 
690 1 0 |a CONTROLLER SYNTHESIS 
690 1 0 |a DOMAIN MODEL 
690 1 0 |a INCREMENTAL DEVELOPMENT 
690 1 0 |a LABELLED TRANSITION SYSTEMS 
690 1 0 |a MODAL TRANSITION SYSTEMS 
690 1 0 |a PROBLEM DOMAIN 
690 1 0 |a REALISABILITY 
690 1 0 |a ARTIFICIAL INTELLIGENCE 
690 1 0 |a CONTROLLERS 
700 1 |a Braberman, V. 
700 1 |a Piterman, N. 
700 1 |a Uchitel, S. 
711 2 |c Paris  |d 27 August 2012 through 31 August 2012  |g Código de la conferencia: 92488 
773 0 |d 2012  |g v. 7436 LNCS  |h pp. 155-170  |p Lect. Notes Comput. Sci.  |n Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)  |x 03029743  |w (AR-BaUEN)CENRE-983  |z 9783642327582  |t 18th International Symposium on Formal Methods, FM 2012 
856 4 1 |u https://www.scopus.com/inward/record.uri?eid=2-s2.0-84865995885&doi=10.1007%2f978-3-642-32759-9_15&partnerID=40&md5=2cfdd1152b35e5dbc9d661d6ca96ae64  |y Registro en Scopus 
856 4 0 |u https://doi.org/10.1007/978-3-642-32759-9_15  |y DOI 
856 4 0 |u https://hdl.handle.net/20.500.12110/paper_03029743_v7436LNCS_n_p155_DIppolito  |y Handle 
856 4 0 |u https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_03029743_v7436LNCS_n_p155_DIppolito  |y Registro en la Biblioteca Digital 
961 |a paper_03029743_v7436LNCS_n_p155_DIppolito  |b paper  |c PE 
962 |a info:eu-repo/semantics/article  |a info:ar-repo/semantics/artículo  |b info:eu-repo/semantics/publishedVersion 
963 |a VARI 
999 |c 70282 

Ejemplares similares