?. Translate, A. Program, and . Fotl, TSpass syntax) using (-t) argument: root@root/:$ python aalc -i examples/tuto0

[. Aktug and K. Naliuka, ConSpec ??? A Formal Language for Policy Specification, Electronic Notes in Theoretical Computer Science, vol.197, issue.1, pp.45-58, 2008.
DOI : 10.1016/j.entcs.2007.10.013

E. Alata, M. Dacier, Y. Deswarte, M. Kaaâniche, K. Kortchinsky et al., Collection and analysis of attack data based on honeypots deployed on the Internet, pp.79-91, 2006.
DOI : 10.1007/978-0-387-36584-8_7

URL : https://hal.archives-ouvertes.fr/hal-00140390

P. Allan, A. Avgustinov, L. Simon-christensen, S. Hendren, O. Kuzins et al., Adding Trace Matching with Free Variables to AspectJ, Proceedings of the 20th Annual ACM SIG- PLAN Conference on Object-oriented Programming, Systems, Languages, and Applications. OOPSLA '05, 2005.

]. J. And74 and . Anderson, Computer Security Technology Planning Study, 1974.

C. A. Ardagna, PrimeLife Policy Language, 2009.

A. Azraoui, K. Elkhiyaoui, M. Önen, K. Bernsmed, A. S. et al., An Accountability Policy Language Revised Selected Papers, » In: Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance: 9th International Workshop, DPM 2014, 7th International Workshop, SETOP 2014, and 3rd International Workshop, pp.319-326978, 2014.
DOI : 10.1007/978-3-319-17016-9_21

R. Babaee and S. Babamir, Runtime verification of service-oriented systems: a well-rounded survey, International Journal of Web and Grid Services, vol.9, issue.3, 2013.
DOI : 10.1504/IJWGS.2013.055699

[. Bacchus and F. Kabanza, « Planning for temporally extended goals, » In: Annals of Mathematics and Artificial Intelligence, vol.221, p.1018985923441, 1998.

A. Barros, D. Basin, F. Klaedtke, and S. Müller, Handbook of Service Description: USDL and Its Methods, Policy Monitoring in First-Order Temporal Logic. » In: Computer Aided Verification: 22nd International Conference Proceedings. Ed. by Tayssir Touili, 2010.
DOI : 10.1007/978-1-4614-1864-1

[. Bauer, J. Küster, and G. Vegliach, From Propositional to First-Order Monitoring, Runtime Verification: 4th International Conference Proceedings, pp.978-981, 2013.
DOI : 10.1007/978-3-642-40787-1_4

URL : http://arxiv.org/pdf/1303.3645

[. Bauer, J. Küster, and G. Vegliach, « The ins and outs of first-order runtime verification. » English In: Formal Methods in System Design 46, pp.10703-10718, 2015.

[. Bauer, M. Leucker, C. Schallhart, . «-runtime, L. Verification-for et al., Runtime Verification for LTL and TLTL, ACM Transactions on Software Engineering and Methodology, vol.20, issue.4, pp.1-14, 2011.
DOI : 10.1145/2000799.2000800

URL : http://www4.in.tum.de/~leucker/Documents/Leucker/tosem09_prelim.pdf

Y. Moritz, A. Becker, L. Malkis, and . Bussard, « A Practical Generic Privacy Language, Somesh Jha and Anish Mathuria, vol.6503, pp.125-139, 2010.

[. Benghabrit, H. Grall, J. Royer, and M. Sellami, Accountability for Abstract Component Design, 2014 40th EUROMICRO Conference on Software Engineering and Advanced Applications, pp.213-220, 2014.
DOI : 10.1109/SEAA.2014.68

URL : https://hal.archives-ouvertes.fr/hal-00987165

D. Travis, A. I. Breaux, and . Anton, « Deriving Semantic Models from Privacy Policies. » In: Sixth IEEE International Workshop on Policies for Distributed Systems and Networks (POLICY '05), POLICY, vol.12, pp.67-76, 2005.

[. Brunel, J. Bodeveix, and M. Filali, A State/Event Temporal Deontic Logic, pp.85-100, 2006.
DOI : 10.1007/11786849_9

D. Butin, M. Chicote, and D. L. Métayer, « Strong Accountability: Beyond Vague Promises. » In: Reloading Data Protection: Multidisciplinary Insights and Contemporary Challenges, pp.343-369, 2014.
DOI : 10.1007/978-94-007-7540-4_16

D. Butin and D. L. Métayer, Log Analysis for Data Protection Accountability, FM 2014: Formal Methods: 19th International Symposium Proceedings, pp.163-178, 2014.
DOI : 10.1007/978-3-319-06410-9_12

URL : https://hal.archives-ouvertes.fr/hal-00984308

[. Buyya, J. Broberg, and A. M. Goscinski, Cloud Computing Principles and Paradigms, p.9780470887998, 2011.

[. Castañeda, The Paradoxes of Deontic Logic: The Simplest Solution to all of them in one Fell Swoop. » In: New Studies in Deontic Logic: Norms, Actions, and the Foundations of Ethics, pp.978-94, 1981.

F. Chen and G. Ro?u, Tools and Algorithms for the Construction and Analysis of Systems Held as Part of the Joint European Conferences on Theory and Practice of Software, Parametric Trace Slicing and Monitoring. 15th International Conference Proceedings, pp.246-261978, 2009.

J. Chomicki and . Efficient, Efficient checking of temporal integrity constraints using bounded history encoding, ACM Transactions on Database Systems, vol.20, issue.2, pp.149-186, 1995.
DOI : 10.1145/210197.210200

[. Chowdhury, A. Gampe, J. Niu, J. Von-ronne, J. Bennatt et al., Privacy promises that can be kept, Proceedings of the 18th ACM symposium on Access control models and technologies, SACMAT '13
DOI : 10.1145/2462410.2462423

S. Cranen, J. Groote, J. A. Keiren, F. M. Stappers, . Erikp et al., An Overview of the mCRL2 Toolset and Its Recent Advances, Lecture Notes in Computer Science, vol.7795, pp.199-213, 2013.
DOI : 10.1007/978-3-642-36742-7_15

[. Damianou, N. Dulay, E. Lupu, and M. Sloman, The Ponder Policy Specification Language, Lecture Notes in Computer Science, vol.1995, pp.18-38, 2001.
DOI : 10.1007/3-540-44569-2_2

G. De, G. , and M. Y. Vardi, « Linear Temporal Logic and Linear Dynamic Logic on Finite Traces, Proceedings of the Twenty-Third International Joint Conference on Artificial Intelligence. IJCAI '13, pp.854-860, 2013.

[. Deyoung, D. Garg, L. Jia, D. Kaynar, and A. Datta, Experiences in the logical specification of the HIPAA and GLBA privacy laws, Proceedings of the 9th annual ACM workshop on Privacy in the electronic society, WPES '10, pp.73-82, 2010.
DOI : 10.1145/1866919.1866930

E. Dir95-]-directive, Directive 95/46/EC of the European Parliament and of the Council of 24 October 1995 on the protection of individuals with regard to the processing of personal data and on the free movement of such data, 1995.

C. Dixon, M. Fisher, B. Konev, and A. Lisitsa, « Efficient First-Order Temporal Logic for Infinite- State Systems, p.702036, 2007.

S. Etalle and W. H. Winsborough, « A posteriori compliance control. » In: SACMAT 2007, pp.11-20, 2007.
DOI : 10.5771/9783845238098-125

URL : https://ris.utwente.nl/ws/files/5488410/sacmat53-etalle.pdf

J. Feigenbaum, A. D. Jaggard, R. N. Wright, and H. Xiao, Systematizing "Accountability" in Computer Science, 2012.

F. Feldman, A Simpler Solution to the Paradoxes of Deontic Logic, Philosophical Perspectives, vol.4, 1990.
DOI : 10.2307/2214197

U. [. Fernández-gago, C. Hustadt, M. Dixon, B. Fisher, and . Konev, « First-Order Temporal Verification in Practice . » En, In: Journal of Automated Reasoning, vol.343, pp.295-321, 2006.

M. Fisher, Temporal Representation and Reasoning . » In: Handbook of Knowledge Representation, pp.513-550, 2008.

M. Fisher, An Introduction to Practical Formal Methods using Temporal Logic, 2011.
DOI : 10.1002/9781119991472

P. Gastin and N. Sznajder, « Decidability of wellconnectedness for distributed synthesis. » In: Information Processing Letters 112, pp.963-968, 2012.

[. Genon, T. Massart, and C. Meuter, « Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences is Needed to Model-check Traces. » In: Proceedings of the 14th International Conference on Formal Methods. FM'06, pp.557-572, 2006.

A. Goodloe and L. Pike, Monitoring Distributed Real- Time Systems: A Survey and Future Directions, 2010.

A. Carl, M. J. Gunter, S. G. May, and . Stubblebine, « A Formal Privacy System and Its Application to Location Based Services. » In: Privacy Enhancing Technologies: 4th International Workshop Revised Selected Papers, 2004.

R. [. Halle and . Villemaire, Runtime Monitoring of Message-Based Workflows with Data, 2008 12th International IEEE Enterprise Distributed Object Computing Conference, pp.63-72, 2008.
DOI : 10.1109/EDOC.2008.32

J. Hansen, G. Pigozzi, and L. Van-der-torre, « Ten Philosophical Problems in Deontic Logic » In: Normative Multi-agent Systems, van der Torre, and Harko Verhagen. Dagstuhl Seminar Proceedings 07122. Dagstuhl, Germany: Internationales Begegnungs-und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, p.941, 2007.

[. Hilty, A. Pretschner, D. A. Basin, C. Schaefer, and T. Walter, A Policy Language for Distributed Usage Control, Lecture Notes in Computer Science, vol.4734, pp.531-546, 2007.
DOI : 10.1007/978-3-540-74835-9_35

[. Jagadeesan, A. Jeffrey, C. Pitcher, and J. Riely, Towards a Theory of Accountability and Audit, pp.152-167, 2009.
DOI : 10.1145/1288783.1288786

[. Kazhamiakin and M. Pistore, Analysis of Realizability Conditions for Web Service Choreographies, 26th IFIP WG 6.1 International Conference, pp.61-76, 2006.
DOI : 10.1145/1066677.1066867

S. Kerrigan and K. H. Law, Logic-based regulation compliance-assistance, Proceedings of the 9th international conference on Artificial intelligence and law , ICAIL '03, pp.126-135, 2003.
DOI : 10.1145/1047788.1047820

URL : http://eil.stanford.edu/publications/shawn_kerrigan/ICAIL2003-kerrigan.pdf

[. Lamanna, J. Skene, and W. Emmerich, « SLAng: A Language for Defining Service Level Agreements . » In: Proceedings of the The Ninth IEEE Workshop on Future Trends of Distributed Computing Systems. FT- DCS '03, pp.100-100, 2003.

. [. Laroussinie, . Ph, and . Schnoebelen, « A hierarchy of temporal logics with past, » In: Theoretical Computer Science, vol.1482, pp.303-324, 1995.

L. Laure, Le Règlement Général sur la Protection des Données (RGPD)

[. Ludwig and U. Hustadt, « Implementing a fair monodic temporal logic prover, AI Commun, vol.23, pp.2-3, 2010.

T. Mather, S. Kumaraswamy, and S. Latif, Cloud Security and Privacy: An Enterprise Perspective on Risks and Compliance, pp.596802765-9780596802769, 2009.

C. [. May, I. Gunter, and . Lee, Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies, 19th IEEE Computer Security Foundations Workshop (CSFW'06), pp.97-107, 1924.
DOI : 10.1109/CSFW.2006.24

URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=1269&context=cis_papers

T. Ashley and . Mcneile, « Protocol contracts with application to choreographed multiparty collaborations. » In: Service Oriented Computing and Applications 4, pp.109-136, 2010.

[. Métayer, « A Formal Privacy Management Framework » In: Formal Aspects in Security and Trust: 5th International Workshop, FAST Revised Selected Papers, Malaga, vol.isbn, pp.162-176, 2008.

K. D. Mitnick and W. L. Simon, The Art of Deception: Controlling the Human Element of Security, p.76454280, 2003.

K. D. Mitnick and W. L. Simon, The art of intrusion, Indianapolis, p.764589423, 2006.

[. Standard, eXtensible Access Control Markup Language (XACML) Version 3.0. 22, 2013.

[. Services-secure and . Exchange, WS-SX) TC. WS- Trust 1.4

S. Pearson and N. Wainwright, An interdisciplinary approach to accountability for future internet service provision, International Journal of Trust Management in Computing and Communications, vol.1, issue.1, pp.52-72, 2013.
DOI : 10.1504/IJTMCC.2013.052524

G. Piolle and Y. Demazeau, « Representing privacy regulations with deontico-temporal operators. » In: Web Intelligence and Agent Systems 9, pp.209-226, 2011.

A. «. Pnueli, The temporal logic of programs, 18th Annual Symposium on Foundations of Computer Science (sfcs 1977), pp.46-57, 1977.
DOI : 10.1109/SFCS.1977.32

R. Ramanujam and S. Sheerazuddin, A Local Logic for Realizability in Web Service Choreographies, Proceedings 10th International Workshop on Automated Specification and Verification of Web Systems, pp.16-35, 2014.
DOI : 10.1007/3-540-60218-6_33

[. Rumbaugh, I. Jacobson, and G. Booch, Unified Modeling Language Reference Manual, The (2Nd Edition ). Pearson Higher Education, p.321245628, 2004.

A. Schedler, Self-Restraining State: Power and Accountability in New Democracies, 1999.

M. A. Scholl, K. M. Stine, J. Hash, P. Bowen, L. A. Johnson et al., SP 800-66 Rev. 1. An Introductory Resource Guide for Implementing the Health Insurance Portability and Accountability Act (HIPAA) Security Rule, 2008.

[. Sen, G. Ro?u, and G. Agha, Generating Optimal Linear Temporal Logic Monitors by Coinduction, Advances in Computing Science ? ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation: 8th Asian Computing Science Conference Proceedings, pp.260-275978, 2003.
DOI : 10.1007/978-3-540-40965-6_17

URL : http://gureni.cs.uiuc.edu/~grosu/download/ltl2dfa.ps

[. Sen, A. Vardhan, G. Agha, and G. Rosu, Efficient decentralized monitoring of safety in distributed systems, Proceedings. 26th International Conference on Software Engineering, pp.418-427, 2004.
DOI : 10.1109/ICSE.2004.1317464

[. Sen, A. Vardhan, G. Agha, and G. Ro?u, Decentralized runtime analysis of multithreaded applications, Proceedings 20th IEEE International Parallel & Distributed Processing Symposium, 2006.
DOI : 10.1109/IPDPS.2006.1639591

Y. Shen, J. Li, Z. Wang, T. Su, B. Fang et al., Runtime Verification by Convergent Formula Progression, 2014 21st Asia-Pacific Software Engineering Conference, pp.255-262, 2014.
DOI : 10.1109/APSEC.2014.47

A. [. Sundareswaran, D. Squicciarini, and . Lin, Ensuring Distributed Accountability for Data Sharing in the Cloud, IEEE Transactions on Dependable and Secure Computing, vol.9, issue.4, pp.556-568, 2012.
DOI : 10.1109/TDSC.2012.26

]. P3p and . W3c, Platform for Privacy Preferences

]. L. Zha+10, T. Zhao, J. Tang, T. Wu, and . Xu, « Runtime Verification with Multi-valued Formula Rewriting, Theoretical Aspects of Software Engineering (TASE), 2010 4th IEEE International Symposium on. 2010, pp.77-86

Y. Kathiresshan, « A survey of accountability in computer networks and distributed systems, 2012.

J. Zou, Y. Wang, and K. Lin, A Formal Service Contract Model for Accountable SaaS and Cloud Services, 2010 IEEE International Conference on Services Computing, 2010.
DOI : 10.1109/SCC.2010.85