Abstract:
The problem of automatically constructing a software component such that when executed in a given environment satisfies a goal, is recurrent in software engineering. Controller synthesis is a field which fits into this vision. In this paper we study controller synthesis for partially observable LTS models. We exploit the link between partially observable control and non-determinism and show that, unlike fully observable LTS or Kripke structure control problems, in this setting the existence of a solution depends on the interaction model between the controller-to-be and its environment. We identify two interaction models, namely Interface Automata and Weak Interface Automata, define appropriate control problems and describe synthesis algorithms for each of them. © 1976-2012 IEEE.
Registro:
Documento: |
Artículo
|
Título: | Interaction Models and Automated Control under Partial Observable Environments |
Autor: | Ciolek, D.; Braberman, V.; Dippolito, N.; Piterman, N.; Uchitel, S. |
Filiación: | Departamento de Computacion, Universidad de Buenos Aires, Argentina Department of Computing, Imperial College, London, United Kingdom Department of Computer Science, University of Leicester, Leicester, United Kingdom
|
Palabras clave: | controller synthesis; imperfect-information games; LTS; Automata theory; Software engineering; Automated control; Controller synthesis; Existence of a solutions; Imperfect information games; Interaction model; Interface automata; Software component; Synthesis algorithms; Controllers |
Año: | 2017
|
Volumen: | 43
|
Número: | 1
|
Página de inicio: | 19
|
Página de fin: | 33
|
DOI: |
http://dx.doi.org/10.1109/TSE.2016.2564959 |
Título revista: | IEEE Transactions on Software Engineering
|
Título revista abreviado: | IEEE Trans Software Eng
|
ISSN: | 00985589
|
CODEN: | IESED
|
Registro: | https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_00985589_v43_n1_p19_Ciolek |
Referencias:
- Letier, E., Heaven, W., Requirements modelling by synthesis of deontic input-output automata (2013) Proc. Int. Conf. Softw. Eng., pp. 592-601
- Jackson, M., (1995) Software Requirements & Specifications: A Lexicon of Practice Principles and Prejudices, , New York NY USA: ACM Press
- D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesizing nonanomalous event-based controllers for liveness goals (2013) ACM Trans. Softw. Eng. Methodology, 22 (1), pp. 91-936
- Heaven, W., Sykes, D., Magee, J., Kramer, J., A case study in goal-driven architectural adaptation (2009) Software Engineering for Self-Adaptive Systems, pp. 109-127. , B. H. Cheng, R. Lemos, H. Giese, P. Inverardi, and J. Magee, Eds. New York, NY, USA: Springer-Verlag
- Pistore, M., Barbon, F., Bertoli, P., Shaparau, D., Traverso, P., Planning and monitoring web service composition (2004) Proc. 11th Int. Conf. Artif. Intell.: Methodology, Syst., Appl., pp. 106-115
- Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Saar, Y., Synthesis of reactive(1) designs (2012) J. Comput. Syst. Sci., 78 (3), pp. 911-938
- Giannakopoulou, D., Magee, J., Fluent model checking for event-based systems (2003) Proc. 9th Eur. Softw. Eng. Conf. Held Jointly 11th ACM SIGSOFT Int. Symp. Found. Softw. Eng., pp. 257-266
- Van Lamsweerde, A., Goal-oriented requirements engineering: A guided tour (2001) Proc. 5th IEEE Int. Symp. Requirements Eng., pp. 249-262
- Hoare, C.A.R., Communicating sequential processes (1978) Commun. ACM, 21 (8), pp. 666-677
- De Alfaro, L., Henzinger, T.A., Interface automata (2001) Proc. 8th Eur. Softw. Eng. Conf. Held Jointly 9th ACM SIGSOFT Int. Symp. Found. Softw. Eng., pp. 109-120
- Bierhoff, K., Aldrich, J., Lightweight object specification with typestates (2005) Proc. 10th Eur. Softw. Eng. Conf. Held Jointly 13th ACM SIGSOFT Int. Symp. Found. Softw. Eng., pp. 217-226
- Caso, G.D., Braberman, V., Garbervetsky, D., Uchitel, S., Enabledness-based program abstractions for behavior validation (2013) ACM Trans. Softw. Eng. Methodol., 22 (3), pp. 251-2546
- Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., Henzinger, T.A., Strategy construction for parity games with imperfect information (2010) Inf. Comput., 208 (10), pp. 1206-1220
- Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D., (2006) Compilers: Princi-ples, Techniques, and Tools, 2nd Ed, , White Plains, NY, USA: Longman, Inc
- Keller, R.M., Formal verification of parallel programs (1976) Commun. ACM, 19 (7), pp. 371-384
- Reif, J.H., Universal games of incomplete information (1979) Proc. 11th Annu. ACM Symp. Theory Comput., pp. 288-308
- Thistle, J.G., Lamouchi, H.M., Effective control synthesis for partially observed discrete-event systems (2009) SIAM J. Control Optim., 48 (3), pp. 1858-1887
- Inverardi, P., Tivoli, M., A reuse-based approach to the correct and automatic composition of web-services (2007) Proc. Int. Workshop Eng. Softw. Serv. Pervasive Environ.: Conjunction 6th ESEC/FSE Joint Meeting, pp. 29-33
- D'Ippolito, N., Braberman, V., Piterman, N., Uchitel, S., Synthesis of live behaviour models for fallible domains (2011) Proc. 33rd Int. Conf. Softw. Eng., pp. 211-220
- D'Ippolito, N., Fischbein, D., Chechik, M., Uchitel, S., MTSA: The modal transition system analyser (2008) Proc. 23rd IEEE/ACM Int. Conf. Automated Softw. Eng., pp. 475-476
- Foster, H., Uchitel, S., Magee, J., Kramer, J., Model-based verification of web service compositions (2003) Proc. 18th IEEE Int. Conf. Automated Softw. Eng., pp. 152-161
- Piterman, N., Pnueli, A., Sa'Ar, Y., Synthesis of reactive(1) designs (2006) Proc. 7th Int. Conf. Verification, Model Checking Abstract Interpretation, pp. 364-380
- D'Ippolito, N.R., Braberman, V., Piterman, N., Uchitel, S., Synthesis of live behaviour models (2010) Proc. 18th ACM SIGSOFT Int. Symp. Found. Softw. Eng., pp. 211-220
- Kuijper, W., Pol, J., Compositional control synthesis for partially observable systems (2009) Proc. 20th Int. Conf. Concurrency Theory, pp. 431-447
- Chatterjee, K., Henzinger, T.A., Jobstmann, B., Environment assumptions for synthesis (2008) Proc. 19th Int. Conf. Concurrency Theory, pp. 147-161
- Thistle, J.G., Wonham, W.M., Control of infinite behavior of finite automata (1994) SIAM J. Control Optim., 32 (4), pp. 1075-1097
- Klein, J., Baier, C., Klüppelholz, S., Compositional construction of most general controllers (2015) Acta Inf., 52 (4-5), pp. 443-482
- Jiang, S., Kumar, R., Supervisory control of discrete event systems with CTL∗ temporal logic specifications (2006) SIAM J. Control Optim., 44 (6), pp. 2079-2103
- Kupferman, O., Vardi, M.Y., Synthesis with incomplete information (2000) Advances in Temporal Logic, pp. 109-127. , H. Barringer, M. Fisher, D. Gabbay, and G. Gough, Eds. Netherlands: Springer
- Arnold, A., Vincent, A., Walukiewicz, I., Games for synthesis of controllers with partial observation (2003) Theoretical Comput. Sci., 303 (1), pp. 7-34
- Baeten, J.C.M., Van Beek, B., Van Hulst, A., Markovski, J., A process algebra for supervisory coordination (2011) Proc. 1st Int. Workshop Process Algebra Coordination, pp. 36-55
- De Nicola, R., Hennessy, M.C., Testing equivalences for proc-esses (1984) Theoretical Comput. Sci., 34 (1), pp. 83-133
- Honda, K., Vasconcelos, V.T., Kubo, M., Language primitives and type discipline for structured communication-based pro-gramming (1998) Proc. 7th Eur. Symp. Program.: Program. Lang. Syst., pp. 122-138
- Castagna, G., Gesbert, N., Padovani, L., A theory of contracts for web services (2009) ACM Trans. Program. Lang. Syst., 31 (5), pp. 191-1961
- Mehta, N.R., Medvidovic, N., Phadke, S., Towards a taxonomy of software connectors (2000) Proc. 22nd Int. Conf. Softw. Eng., pp. 178-187
Citas:
---------- APA ----------
Ciolek, D., Braberman, V., Dippolito, N., Piterman, N. & Uchitel, S.
(2017)
. Interaction Models and Automated Control under Partial Observable Environments. IEEE Transactions on Software Engineering, 43(1), 19-33.
http://dx.doi.org/10.1109/TSE.2016.2564959---------- CHICAGO ----------
Ciolek, D., Braberman, V., Dippolito, N., Piterman, N., Uchitel, S.
"Interaction Models and Automated Control under Partial Observable Environments"
. IEEE Transactions on Software Engineering 43, no. 1
(2017) : 19-33.
http://dx.doi.org/10.1109/TSE.2016.2564959---------- MLA ----------
Ciolek, D., Braberman, V., Dippolito, N., Piterman, N., Uchitel, S.
"Interaction Models and Automated Control under Partial Observable Environments"
. IEEE Transactions on Software Engineering, vol. 43, no. 1, 2017, pp. 19-33.
http://dx.doi.org/10.1109/TSE.2016.2564959---------- VANCOUVER ----------
Ciolek, D., Braberman, V., Dippolito, N., Piterman, N., Uchitel, S. Interaction Models and Automated Control under Partial Observable Environments. IEEE Trans Software Eng. 2017;43(1):19-33.
http://dx.doi.org/10.1109/TSE.2016.2564959