--- abstract: 'TLA+ and B share the common base of predicate logic, arithmetic and set theory. However, there are still considerable differences, such as very different approaches to typing and modularization. There is also considerable difference in the available tool support. In this paper, we present a translation of the non-temporal part of TLA+ to B, which makes it possible to feed TLA+ specifications into existing tools for B. Part of this translation must include a type inference algorithm, in order to produce typed B specifications. There are many other tricky aspects, such as translating modules as well as let and if-then-else expressions. We also present an integration of our translation into ProB. ProB thus provides a complementary tool to the explicit state model checker TLC, with convenient animation and constraint solving for TLA+. We also present a series of case studies, highlighting the complementarity to TLC. In particular, we highlight the sometimes dramatic difference in performance when it comes to solving complicated constraints in TLA+.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: [] creators_name: - family: Hansen given: Dominik honourific: '' lineage: '' - family: Leuschel given: Michael honourific: '' lineage: '' data_type: ~ date: 2012 date_type: ~ datestamp: 2012-09-11 18:42:09 department: ~ dir: disk0/00/00/04/50 divisions: [] edit_lock_since: ~ edit_lock_until: 0 edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 450 event_dates: ~ event_location: ~ event_title: Proceedings iFM'2012 event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: ~ full_text_status: none funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: ~ issn: ~ item_issues_comment: [] item_issues_count: ~ item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2012-09-11 18:42:09 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: ~ official_url: http://www.stups.uni-duesseldorf.de/mediawiki/images/1/1c/Pub-HansenLeuschelTLA2012.pdf output_media: ~ pagerange: 24-38 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: paper producers_id: [] producers_name: [] projects: [] publication: ~ publisher: Springer refereed: ~ referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 7 series: LNCS 7321 skill_areas: [] source: ~ status_changed: 2012-09-11 18:42:09 subjects: - ADVANCE succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Translating TLA+ to B for Validation with ProB type: conference_item userid: 1 volume: ~