{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:30:02Z","timestamp":1725575402523},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_14","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T05:06:38Z","timestamp":1295240798000},"page":"184-198","source":"Crossref","is-referenced-by-count":6,"title":["Access Nets: Modeling Access to Physical Spaces"],"prefix":"10.1007","author":[{"given":"Robert","family":"Frohardt","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bor-Yuh Evan","family":"Chang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sriram","family":"Sankaranarayanan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.\u00a0126(2) (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Deters, M., Oliveras, A., Stump, A.: Design and results of the third annual satisfiability modulo theories competition (SMT-Comp 2007). International Journal on Artificial Intelligence Tools\u00a017(4) (2008)","DOI":"10.1142\/S0218213008004060"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-74835-9_3","volume-title":"Computer Security \u2013 ESORICS 2007","author":"L. Bauer","year":"2007","unstructured":"Bauer, L., Garriss, S., Reiter, M.K.: Efficient proving for practical distributed access-control systems. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, p. 193. Springer, Heidelberg (1999)"},{"key":"14_CR5","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking (1999)"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst.\u00a016(5) (1994)","DOI":"10.1145\/186025.186051"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR8","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT solver, \n                  \n                    http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"14_CR9","unstructured":"Ferraiolo, D.F., Kuhn, D.R., Chandramouli, R.: Role-based Access Control (2003)"},{"key":"14_CR10","unstructured":"Frohardt, R., Chang, B.-Y.E., Sankaranarayanan, S.: Access Nets: Modeling access to physical spaces (extended version). Technical Report CU-CS-1076-10, Department of Computer Science, University of Colorado, Boulder (2010)"},{"key":"14_CR11","doi-asserted-by":"crossref","unstructured":"Genrich, H.J., Lautenbach, K.: System modelling with high-level Petri nets. Theor. Comput. Sci.\u00a013(1) (1981)","DOI":"10.1016\/0304-3975(81)90113-4"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-30144-8_19","volume-title":"Information Security","author":"D.P. Guelev","year":"2004","unstructured":"Guelev, D.P., Ryan, M.D., Schobbens, P.-Y.: Model-checking access control policies. In: Zhang, K., Zheng, Y. (eds.) ISC 2004. LNCS, vol.\u00a03225, pp. 219\u2013230. Springer, Heidelberg (2004)"},{"key":"14_CR13","doi-asserted-by":"crossref","unstructured":"Helbing, D., Farkas, I., Vicsek, T.: Simulating dynamical features of escape panic. Nature\u00a0407(6803) (2000)","DOI":"10.1038\/35035023"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Henderson, L.: The statistics of crowd fluids. Nature\u00a0229 (1971)","DOI":"10.1038\/229381a0"},{"key":"14_CR15","unstructured":"Holzmann, G.: The SPIN Model Checker (2003)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Jensen, K.: Coloured Petri nets and the invariant-method. Theor. Comput. Sci.\u00a014(3) (1981)","DOI":"10.1016\/0304-3975(81)90049-9"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Jha, S., Li, N., Tripunitara, M.V., Wang, Q., Winsborough, W.H.: Towards formal verification of role-based access control policies. IEEE Transactions on Dependable and Secure Computing (TDSC)\u00a05(4) (2008)","DOI":"10.1109\/TDSC.2007.70225"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Lovas, G.: Modeling and simulation of pedestrian traffic flow. Transportation Research B\u00a028(6) (1994)","DOI":"10.1016\/0191-2615(94)90013-2"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"Murata, T.: Petri nets: Properties, analysis and applications. Proc. IEEE\u00a077(4) (1989)","DOI":"10.1109\/5.24143"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: From an abstract DPLL procedure to DPLL(T). J. ACM 53(6) (2006)","DOI":"10.1145\/1217856.1217859"},{"key":"14_CR21","doi-asserted-by":"crossref","unstructured":"Pelechano, N., Malkawi, A.: Evacuation simulation models: Challenges in modeling high rise building evacuation with cellular automata approaches. Automation in Construction\u00a017(4) (2008)","DOI":"10.1016\/j.autcon.2007.06.005"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst.\u00a024(3) (2002)","DOI":"10.1145\/514188.514190"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Sampemane, G., Naldurg, P., Campbell, R.H.: Access control for active spaces. In: Computer Security Applications, ACSAC (2002)","DOI":"10.1109\/CSAC.2002.1176306"},{"key":"14_CR24","doi-asserted-by":"crossref","unstructured":"Shen, T.: ESM: A building evacuation simulation model. Building and Environment\u00a040(5) (2005)","DOI":"10.1016\/j.buildenv.2004.08.029"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18275-4_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T22:55:08Z","timestamp":1553381708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}