{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,1,9]],"date-time":"2024-01-09T23:40:30Z","timestamp":1704843630599},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,1,5]],"date-time":"2013-01-05T00:00:00Z","timestamp":1357344000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2014,2]]},"DOI":"10.1007\/s10009-012-0269-3","type":"journal-article","created":{"date-parts":[[2013,1,4]],"date-time":"2013-01-04T14:02:38Z","timestamp":1357308158000},"page":"31-48","source":"Crossref","is-referenced-by-count":12,"title":["Authorized workflow schemas: deciding realizability through $$\\mathsf{LTL }(\\mathsf{F })$$ model checking"],"prefix":"10.1007","volume":"16","author":[{"given":"Jason","family":"Crampton","sequence":"first","affiliation":[]},{"given":"Michael","family":"Huth","sequence":"additional","affiliation":[]},{"given":"Jim Huan-Pu","family":"Kuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2013,1,5]]},"reference":[{"issue":"1","key":"269_CR1","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/s10009-002-0095-0","volume":"5","author":"T Ball","year":"2003","unstructured":"Ball, T., Podelski, A., Rajamani, Sk: Boolean and Cartesian abstraction for model checking C programs. STTT 5(1), 49\u201358 (2003)","journal-title":"STTT"},{"issue":"1","key":"269_CR2","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1145\/300830.300837","volume":"2","author":"E Bertino","year":"1999","unstructured":"Bertino, E., Ferrari, E., Atluri, V.: The specification and enforcement of authorization constraints in workflow management systems. ACM Trans. Inf. Syst. Secur. 2(1), 65\u2013104 (1999)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"269_CR3","doi-asserted-by":"crossref","unstructured":"Bogudlov, I., Lev-Ami, T., Reps, T., Sagiv, M.: Revamping TVLA: making parametric shape analysis competitive. In: Proceedings of the 19th International Conference on Computer Aided Verification, pp. 221\u2013225. Springer, Berlin (2007)","DOI":"10.1007\/978-3-540-73368-3_25"},{"key":"269_CR4","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: CAV, pp. 359\u2013364 (2002)","DOI":"10.1007\/3-540-45657-0_29"},{"key":"269_CR5","doi-asserted-by":"crossref","unstructured":"Crampton, J.: A reference monitor for workflow systems with constrained task execution. In: Proceedings of the 10th ACM Symposium on Access Control Models and Technologies, pp. 38\u201347 (2005)","DOI":"10.1145\/1063979.1063986"},{"key":"269_CR6","doi-asserted-by":"crossref","unstructured":"Crampton, J., Khambhammettu, H.: Delegation and satisfiability in workflow systems. In: Ray, I., Li, N. (eds.) Proceedings of 13th ACM Symposium on Access Control Models and Technologies, pp. 31\u201340 (2008)","DOI":"10.1145\/1377836.1377842"},{"key":"269_CR7","doi-asserted-by":"crossref","unstructured":"Crampton, J., Huth, M.: On the modeling and verification of security-aware and process-aware information systems. In: van der Aalst, W., Accorsi, R. (eds.) Proceedings of BPM Workshop on Workflow Security Audit and Certification. Lecture Notes in Business Information Processing, Clermont-Ferrand, France, August 2011, vol. 100, pp. 423\u2013434. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28115-0_40"},{"key":"269_CR8","unstructured":"Crampton, J., Huth, M.: Synthesizing and verifying plans for constrained workflows: transferring tools from formal methods. In: Bensalem, S., Havelund, K. (eds.) Proceedings of International Workshop on Verification and Validation of Planning and Scheduling Systems, Freiburg, Germany, June 2011"},{"key":"269_CR9","doi-asserted-by":"crossref","unstructured":"Hildebrandt, T.T., Mukkamala, R.R.: Declarative event-based workflow as distributed dynamic condition response graphs. In: PLACES, pp. 59 (2010)","DOI":"10.4204\/EPTCS.69.5"},{"issue":"2","key":"269_CR10","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1007\/s10009-010-0140-3","volume":"12","author":"KY Rozier","year":"2010","unstructured":"Rozier, K.Y., Vardi, M.Y.: LTL satisfiability checking. STTT 12(2), 123\u2013137 (2010)","journal-title":"STTT"},{"key":"269_CR11","doi-asserted-by":"crossref","unstructured":"Rozier, K.Y., Vardi, M.Y.: A multi-encoding approach for LTL symbolic satisfiability checking. In: Formal Methods, pp. 417\u2013431 (2011)","DOI":"10.1007\/978-3-642-21437-0_31"},{"key":"269_CR12","unstructured":"Russell, N.C.: Foundations of Process-Aware Information Systems. PhD thesis, Faculty of Information Technology, Queensland University of Technology (2007)"},{"issue":"2","key":"269_CR13","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1109\/2.485845","volume":"29","author":"R Sandhu","year":"1996","unstructured":"Sandhu, R., Coyne, E.J., Feinstein, H., Youman, C.E.: Role-based access control models. IEEE Comput. 29(2), 38\u201347 (1996)","journal-title":"IEEE Comput."},{"key":"269_CR14","doi-asserted-by":"crossref","unstructured":"Schmidt, D.A., Steffen, B.: Program analysis is model checking of abstract interpretations. In: Proceedings of 5th International Symposium on Static Analysis, pp. 351\u2013380 (1998)","DOI":"10.1007\/3-540-49727-7_22"},{"key":"269_CR15","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"269_CR16","unstructured":"Tan, K., Crampton, J., Gunter, C.: The consistency of task-based authorization constraints in workflow systems. In: Proceedings of 17th IEEE Computer Security Foundations Workshop, pp. 155\u2013169 (2004)"},{"issue":"2","key":"269_CR17","first-page":"99","volume":"23","author":"WMP Aalst van der","year":"2009","unstructured":"van der Aalst, W.M.P., Pesic, M., Schonenberg, H.: Declarative workflows: balancing between flexibility and support. Comput. Sci. R &D 23(2), 99\u2013113 (2009)","journal-title":"Comput. Sci. R &D"},{"key":"269_CR18","doi-asserted-by":"crossref","unstructured":"van der Aalst, W.M.P., ter Hofstede, A.H.M., Kiepuszewski, B., Barros, A.P.: Workflow patterns. Distrib. Parallel Databases 14(1), 5\u201351 (2003)","DOI":"10.1023\/A:1022883727209"},{"key":"269_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115, 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"269_CR20","doi-asserted-by":"crossref","unstructured":"Wang, Q., Li, N.: Satisfiability and resiliency in workflow systems. In: Proceedings of 12th European Symposium on Research in Computer Security, pp. 90\u2013105 (2007)","DOI":"10.1007\/978-3-540-74835-9_7"},{"key":"269_CR21","doi-asserted-by":"crossref","unstructured":"Warner, J., Atluri, V.: Inter-instance authorization constraints for secure workflow management. In: Proceedings of the 11th ACM Symposium on Access Control Models and Technologies, pp. 190\u2013199 (2006)","DOI":"10.1145\/1133058.1133085"},{"key":"269_CR22","doi-asserted-by":"crossref","unstructured":"Westergaard, M.: Better algorithms for analyzing and enacting declarative workflow languages using LTL. In: BPM, pp. 83\u201398 (2011)","DOI":"10.1007\/978-3-642-23059-2_10"},{"key":"269_CR23","doi-asserted-by":"crossref","unstructured":"Winskel, G.: Event structures. In: Advances in Petri Nets, pp. 325\u2013392 (1986)","DOI":"10.1007\/3-540-17906-2_31"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0269-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-012-0269-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-012-0269-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,7]],"date-time":"2019-07-07T23:24:39Z","timestamp":1562541879000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-012-0269-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,1,5]]},"references-count":23,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["269"],"URL":"https:\/\/doi.org\/10.1007\/s10009-012-0269-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,1,5]]}}}