{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:47Z","timestamp":1750306607753,"version":"3.41.0"},"reference-count":26,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T00:00:00Z","timestamp":1427241600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"EPSRC EP\/H017690\/1"},{"name":"Engineering and Physical Sciences Research Council UK"},{"name":"INRIA project Northern European associate teams between INRIA Lille and University of Oxford"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Database Syst."],"published-print":{"date-parts":[[2015,3,25]]},"abstract":"<jats:p>\n            We study verification of systems whose transitions consist of\n            <jats:italic>accesses to a Web-based data source<\/jats:italic>\n            . An access is a lookup on a relation within a relational database, fixing values for a set of positions in the relation. For example, a transition can represent access to a Web form, where the user is restricted to filling in values for a particular set of fields. We look at verifying properties of a schema describing the possible accesses of such a system. We present a language where one can describe the properties of an access path and also specify additional restrictions on accesses that are enforced by the schema. Our main property language, AccessLTL, is based on a first-order extension of linear-time temporal logic, interpreting access paths as sequences of relational structures. We also present a lower-level automaton model, A-automata, into which AccessLTL specifications can compile. We show that AccessLTL and A-automata can express static analysis problems related to \u201cquerying with limited access patterns\u201d that have been studied in the database literature in the past, such as whether an access is relevant to answering a query and whether two queries are equivalent in the accessible data they can return. We prove decidability and complexity results for several restrictions and variants of AccessLTL and explain which properties of paths can be expressed in each restriction.\n          <\/jats:p>","DOI":"10.1145\/2699500","type":"journal-article","created":{"date-parts":[[2015,3,25]],"date-time":"2015-03-25T16:03:43Z","timestamp":1427299423000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Analysis of Schemas with Access Restrictions"],"prefix":"10.1145","volume":"40","author":[{"given":"Michael","family":"Benedikt","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, UK"}]},{"given":"Pierre","family":"Bourhis","sequence":"additional","affiliation":[{"name":"CNRS LIFL University of Lille I and INRIA Lille Nord Europe, France"}]},{"given":"Clemens","family":"Ley","sequence":"additional","affiliation":[{"name":"CNRS LIFL University of Lille I and INRIA Lille Nord Europe, France"}]}],"member":"320","published-online":{"date-parts":[[2015,3,25]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"S. Abiteboul R. Hull and V. Vianu. 1995. Foundations of Databases. Addison-Wesley.   S. Abiteboul R. Hull and V. Vianu. 1995. Foundations of Databases. Addison-Wesley."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.2000.1708"},{"volume-title":"Proceedings of the 13th International Conference on Principles of Knowledge Representation and Reasoning (KR'12)","author":"Belardinelli F.","key":"e_1_2_2_3_1"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1989284.1989309"},{"key":"e_1_2_2_5_1","first-page":"33","article-title":"Dynamic query optimization under access limitations and dependencies","volume":"15","author":"Cal\u00ec A.","year":"2009","journal-title":"J. Univer. Comput. Sci."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87877-3_24"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214049"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/jcss.1997.1452"},{"key":"e_1_2_2_9_1","unstructured":"E. M. Clarke O. Grumberg and D. Peled. 2000. Model Checking. MIT Press.  E. M. Clarke O. Grumberg and D. Peled. 2000. Model Checking. MIT Press."},{"key":"e_1_2_2_10_1","unstructured":"H. Comon M. Dauchet R. Gilleron F. Jacquemard D. Lugiez S. Tison and M. Tommasi. 1997. Tree Automata Techniques and Applications. http:\/\/tata.gforge.inria.fr\/.  H. Comon M. Dauchet R. Gilleron F. Jacquemard D. Lugiez S. Tison and M. Tommasi. 1997. Tree Automata Techniques and Applications. http:\/\/tata.gforge.inria.fr\/."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338626.2338628"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514924"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.11.008"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2006.10.006"},{"volume-title":"Handbook of Theoretical Computer Science","author":"Emerson E.","key":"e_1_2_2_15_1"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1514894.1514922"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2463664.2465221"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"e_1_2_2_19_1","unstructured":"A. Kurucz F. Wolter M. Zakharyaschev and D. M. Gabbay. 2003. Many-Dimensional Modal Logics: Theory and Applications. Elsevier.  A. Kurucz F. Wolter M. Zakharyaschev and D. M. Gabbay. 2003. Many-Dimensional Modal Logics: Theory and Applications. Elsevier."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00778-002-0085-6"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/502030.502032"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1055558.1055601"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/212433.220199"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(02)00029-6"},{"volume-title":"Principles of Database and Knowledge-Base Systems","author":"Ullman J. D.","key":"e_1_2_2_25_1"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2378969.2378974"}],"container-title":["ACM Transactions on Database Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699500","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2699500","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:59Z","timestamp":1750227419000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699500"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,25]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3,25]]}},"alternative-id":["10.1145\/2699500"],"URL":"https:\/\/doi.org\/10.1145\/2699500","relation":{},"ISSN":["0362-5915","1557-4644"],"issn-type":[{"type":"print","value":"0362-5915"},{"type":"electronic","value":"1557-4644"}],"subject":[],"published":{"date-parts":[[2015,3,25]]},"assertion":[{"value":"2012-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}