Get quick answers to your questions about the article from our AI researcher chatbot
{'id': 'https://openalex.org/W2039853888', 'doi': 'https://doi.org/10.1109/tse.1984.5010246', 'title': 'Protocol Verification via Projections', 'display_name': 'Protocol Verification via Projections', 'publication_year': 1984, 'publication_date': '1984-07-01', 'ids': {'openalex': 'https://openalex.org/W2039853888', 'doi': 'https://doi.org/10.1109/tse.1984.5010246', 'mag': '2039853888'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.1109/tse.1984.5010246', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S8351582', 'display_name': 'IEEE Transactions on Software Engineering', 'issn_l': '0098-5589', 'issn': ['0098-5589', '1939-3520', '2326-3881'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310320439', 'host_organization_name': 'IEEE Computer Society', 'host_organization_lineage': ['https://openalex.org/P4310320439', 'https://openalex.org/P4310319808'], 'host_organization_lineage_names': ['IEEE Computer Society', 'Institute of Electrical and Electronics Engineers'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'journal-article', 'indexed_in': ['crossref'], 'open_access': {'is_oa': False, 'oa_status': 'closed', 'oa_url': None, 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5101865930', 'display_name': 'Simon S. Lam', 'orcid': 'https://orcid.org/0000-0002-4447-6401'}, 'institutions': [{'id': 'https://openalex.org/I86519309', 'display_name': 'The University of Texas at Austin', 'ror': 'https://ror.org/00hj54h04', 'country_code': 'US', 'type': 'education', 'lineage': ['https://openalex.org/I86519309']}], 'countries': ['US'], 'is_corresponding': False, 'raw_author_name': 'Simon S. Lam', 'raw_affiliation_strings': ['Department of Computer Science, University of Texas, Austin, TX 78712;'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Science, University of Texas, Austin, TX 78712;', 'institution_ids': ['https://openalex.org/I86519309']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5102709643', 'display_name': 'A. Udaya Shankar', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I66946132', 'display_name': 'University of Maryland, College Park', 'ror': 'https://ror.org/047s2c258', 'country_code': 'US', 'type': 'education', 'lineage': ['https://openalex.org/I66946132']}], 'countries': ['US'], 'is_corresponding': False, 'raw_author_name': 'A. Udaya Shankar', 'raw_affiliation_strings': ['Department of Computer Sciences, University of Texas, Austin, TX 78712.; Department of Computer Science, University of Maryland, College Park, MD 20742.'], 'affiliations': [{'raw_affiliation_string': 'Department of Computer Sciences, University of Texas, Austin, TX 78712.; Department of Computer Science, University of Maryland, College Park, MD 20742.', 'institution_ids': ['https://openalex.org/I66946132']}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 2, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': None, 'apc_paid': None, 'fwci': 9.746, 'has_fulltext': False, 'cited_by_count': 222, 'citation_normalized_percentile': {'value': 0.971091, 'is_in_top_1_percent': False, 'is_in_top_10_percent': True}, 'cited_by_percentile_year': {'min': 98, 'max': 99}, 'biblio': {'volume': 'SE-10', 'issue': '4', 'first_page': '325', 'last_page': '342'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9952, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9952, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9937, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10683', 'display_name': 'Mass Spectrometry Techniques and Applications', 'score': 0.9862, 'subfield': {'id': 'https://openalex.org/subfields/1607', 'display_name': 'Spectroscopy'}, 'field': {'id': 'https://openalex.org/fields/16', 'display_name': 'Chemistry'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/liveness', 'display_name': 'Liveness', 'score': 0.8637325}, {'id': 'https://openalex.org/keywords/link-control-protocol', 'display_name': 'Link Control Protocol', 'score': 0.669323}, {'id': 'https://openalex.org/keywords/general-inter-orb-protocol', 'display_name': 'General Inter-ORB Protocol', 'score': 0.5821656}, {'id': 'https://openalex.org/keywords/otway–rees-protocol', 'display_name': 'Otway–Rees protocol', 'score': 0.47576708}], 'concepts': [{'id': 'https://openalex.org/C15569618', 'wikidata': 'https://www.wikidata.org/wiki/Q3561421', 'display_name': 'Liveness', 'level': 2, 'score': 0.8637325}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.84151363}, {'id': 'https://openalex.org/C2780385302', 'wikidata': 'https://www.wikidata.org/wiki/Q367158', 'display_name': 'Protocol (science)', 'level': 3, 'score': 0.80430627}, {'id': 'https://openalex.org/C41150092', 'wikidata': 'https://www.wikidata.org/wiki/Q1826817', 'display_name': 'Link Control Protocol', 'level': 5, 'score': 0.669323}, {'id': 'https://openalex.org/C165751822', 'wikidata': 'https://www.wikidata.org/wiki/Q7894118', 'display_name': 'Universal composability', 'level': 4, 'score': 0.64768004}, {'id': 'https://openalex.org/C75114861', 'wikidata': 'https://www.wikidata.org/wiki/Q594324', 'display_name': 'General Inter-ORB Protocol', 'level': 5, 'score': 0.5821656}, {'id': 'https://openalex.org/C20636137', 'wikidata': 'https://www.wikidata.org/wiki/Q11163', 'display_name': 'User Datagram Protocol', 'level': 4, 'score': 0.5730947}, {'id': 'https://openalex.org/C178248399', 'wikidata': 'https://www.wikidata.org/wiki/Q640435', 'display_name': 'Resource Reservation Protocol', 'level': 4, 'score': 0.5170944}, {'id': 'https://openalex.org/C2780801425', 'wikidata': 'https://www.wikidata.org/wiki/Q5164392', 'display_name': 'Construct (python library)', 'level': 2, 'score': 0.5149951}, {'id': 'https://openalex.org/C12269588', 'wikidata': 'https://www.wikidata.org/wiki/Q132364', 'display_name': 'Communications protocol', 'level': 2, 'score': 0.47658536}, {'id': 'https://openalex.org/C35788789', 'wikidata': 'https://www.wikidata.org/wiki/Q1320237', 'display_name': 'Otway–Rees protocol', 'level': 5, 'score': 0.47576708}, {'id': 'https://openalex.org/C162571340', 'wikidata': 'https://www.wikidata.org/wiki/Q1667988', 'display_name': 'Internet Protocol Control Protocol', 'level': 5, 'score': 0.46910128}, {'id': 'https://openalex.org/C65567647', 'wikidata': 'https://www.wikidata.org/wiki/Q81414', 'display_name': 'Internet protocol suite', 'level': 3, 'score': 0.44871265}, {'id': 'https://openalex.org/C14036430', 'wikidata': 'https://www.wikidata.org/wiki/Q3736076', 'display_name': 'Function (biology)', 'level': 2, 'score': 0.43830195}, {'id': 'https://openalex.org/C120314980', 'wikidata': 'https://www.wikidata.org/wiki/Q180634', 'display_name': 'Distributed computing', 'level': 1, 'score': 0.43762705}, {'id': 'https://openalex.org/C31258907', 'wikidata': 'https://www.wikidata.org/wiki/Q1301371', 'display_name': 'Computer network', 'level': 1, 'score': 0.4294067}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.38645136}, {'id': 'https://openalex.org/C21564112', 'wikidata': 'https://www.wikidata.org/wiki/Q4825885', 'display_name': 'Authentication protocol', 'level': 3, 'score': 0.26417813}, {'id': 'https://openalex.org/C11413529', 'wikidata': 'https://www.wikidata.org/wiki/Q8366', 'display_name': 'Algorithm', 'level': 1, 'score': 0.25333357}, {'id': 'https://openalex.org/C33884865', 'wikidata': 'https://www.wikidata.org/wiki/Q1254335', 'display_name': 'Cryptographic protocol', 'level': 3, 'score': 0.23633549}, {'id': 'https://openalex.org/C110875604', 'wikidata': 'https://www.wikidata.org/wiki/Q75', 'display_name': 'The Internet', 'level': 2, 'score': 0.15891841}, {'id': 'https://openalex.org/C207828512', 'wikidata': 'https://www.wikidata.org/wiki/Q1060131', 'display_name': 'Challenge-Handshake Authentication Protocol', 'level': 4, 'score': 0.1159527}, {'id': 'https://openalex.org/C178489894', 'wikidata': 'https://www.wikidata.org/wiki/Q8789', 'display_name': 'Cryptography', 'level': 2, 'score': 0.095077306}, {'id': 'https://openalex.org/C71924100', 'wikidata': 'https://www.wikidata.org/wiki/Q11190', 'display_name': 'Medicine', 'level': 0, 'score': 0.0}, {'id': 'https://openalex.org/C204787440', 'wikidata': 'https://www.wikidata.org/wiki/Q188504', 'display_name': 'Alternative medicine', 'level': 2, 'score': 0.0}, {'id': 'https://openalex.org/C142724271', 'wikidata': 'https://www.wikidata.org/wiki/Q7208', 'display_name': 'Pathology', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C78458016', 'wikidata': 'https://www.wikidata.org/wiki/Q840400', 'display_name': 'Evolutionary biology', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C136764020', 'wikidata': 'https://www.wikidata.org/wiki/Q466', 'display_name': 'World Wide Web', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C86803240', 'wikidata': 'https://www.wikidata.org/wiki/Q420', 'display_name': 'Biology', 'level': 0, 'score': 0.0}, {'id': 'https://openalex.org/C109297577', 'wikidata': 'https://www.wikidata.org/wiki/Q161157', 'display_name': 'Password', 'level': 2, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.1109/tse.1984.5010246', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S8351582', 'display_name': 'IEEE Transactions on Software Engineering', 'issn_l': '0098-5589', 'issn': ['0098-5589', '1939-3520', '2326-3881'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310320439', 'host_organization_name': 'IEEE Computer Society', 'host_organization_lineage': ['https://openalex.org/P4310320439', 'https://openalex.org/P4310319808'], 'host_organization_lineage_names': ['IEEE Computer Society', 'Institute of Electrical and Electronics Engineers'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 20, 'referenced_works': ['https://openalex.org/W125106562', 'https://openalex.org/W136698625', 'https://openalex.org/W1569590355', 'https://openalex.org/W1584343066', 'https://openalex.org/W1589644552', 'https://openalex.org/W1983934003', 'https://openalex.org/W2001280955', 'https://openalex.org/W2029117638', 'https://openalex.org/W2039853888', 'https://openalex.org/W2097786642', 'https://openalex.org/W2103953153', 'https://openalex.org/W2108313206', 'https://openalex.org/W2130140280', 'https://openalex.org/W2137203882', 'https://openalex.org/W2148881249', 'https://openalex.org/W2153339829', 'https://openalex.org/W30118012', 'https://openalex.org/W4230340979', 'https://openalex.org/W4285719527', 'https://openalex.org/W78755002'], 'related_works': ['https://openalex.org/W72195266', 'https://openalex.org/W3168897635', 'https://openalex.org/W2381123248', 'https://openalex.org/W2358154320', 'https://openalex.org/W2350708904', 'https://openalex.org/W2350536881', 'https://openalex.org/W2294179037', 'https://openalex.org/W2237876205', 'https://openalex.org/W2140626418', 'https://openalex.org/W1600194194'], 'abstract_inverted_index': {'The': [0], 'method': [1, 50, 135], 'of': [2, 12, 21, 24, 96, 133, 140], 'projections': [3], 'is': [4, 51, 72, 83, 108, 148], 'a': [5, 22, 76, 138, 151], 'new': [6], 'approach': [7], 'to': [8, 62, 85, 127, 136], 'reduce': [9], 'the': [10, 97, 102, 111, 141], 'complexity': [11], 'analyzing': [13], 'nontrivial': [14], 'communication': [15, 28], 'protocols.': [16], 'A': [17], 'protocol': [18, 25, 71, 81, 99, 107, 113, 122, 147], 'system': [19, 82, 100], 'consists': [20], 'network': [23], 'entities': [26, 31], 'and': [27, 93, 114], 'channels.': [29], 'Protocol': [30], 'interact': [32], 'by': [33], 'exchanging': [34], 'messages': [35, 38], 'through': [36], 'channels;': [37], 'in': [39, 150], 'transit': [40], 'may': [41], 'be': [42, 86, 117], 'lost,': [43], 'duplicated': [44], 'as': [45, 47], 'well': [46], 'reordered.': [48], 'Our': [49], 'intended': [52], 'for': [53, 66], 'protocols': [54, 65], 'with': [55], 'several': [56], 'distinguishable': [57], 'functions.': [58], 'We': [59], 'show': [60], 'how': [61], 'construct': [63], 'image': [64, 70, 80, 106], 'each': [67], 'function.': [68, 104], 'An': [69, 79, 105, 131], 'specified': [73], 'just': [74], 'like': [75], 'real': [77], 'protocol.': [78], 'said': [84], 'faithful': [87], 'if': [88], 'it': [89], 'preserves': [90], 'all': [91], 'safety': [92], 'liveness': [94], 'properties': [95], 'original': [98, 112], 'concerning': [101], 'projected': [103], 'smaller': [109], 'than': [110], 'can': [115], 'typically': [116], 'more': [118], 'easily': [119], 'analyzed.': [120], 'Two': [121], 'examples': [123], 'are': [124], 'employed': [125], 'herein': [126], 'illustrate': [128], 'our': [129], 'method.': [130], 'application': [132], 'this': [134], 'verify': [137], 'version': [139], 'high-level': [142], 'data': [143], 'link': [144], 'control': [145], '(HDLC)': [146], 'described': [149], 'companion': [152], 'paper.': [153]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2039853888', 'counts_by_year': [{'year': 2020, 'cited_by_count': 2}, {'year': 2018, 'cited_by_count': 1}, {'year': 2016, 'cited_by_count': 1}, {'year': 2015, 'cited_by_count': 3}, {'year': 2014, 'cited_by_count': 1}, {'year': 2013, 'cited_by_count': 3}, {'year': 2012, 'cited_by_count': 2}], 'updated_date': '2024-12-24T15:10:41.749838', 'created_date': '2016-06-24'}