一种基于TLA的解决N皇后问题的方法  

A Method to Solve N-Queens Problem Based on TLA+

作　　者：台亚非 龙士工[2] 

机构地区：[1]贵州大学理学院,贵州贵阳550025 [2]贵州大学计算机科学与信息学院,贵州贵阳550025

出　　处：《贵州大学学报（自然科学版）》2016年第1期86-88,共3页Journal of Guizhou University:Natural Sciences

基　　金：国家自然科学基金项目资助(61163001)

摘　　要：行为时序逻辑语言(TLA+)是一种在模型检测范围内能够表达模型程序和逻辑规约的语言。N皇后问题是一个久远的问题,回溯法是解决该问题一种经典的方法。本文提出如何用行为时序逻辑语言TLA+去描述N皇后问题,然后使用Toolbox工具去检测n=5时该问题的全部解。The temporal logic of actions （TLA） is a new sphere of model checking that can express model pro- gram and logic rule in one language. N-Queens Problem is an old puzzle. The backtracking algorithm is the clas- sic method for solving problem. How to write TLA language to specify N-Queens was presented, then use Toolbox describe all solutions when n equal to 5.

关 键 词：行为时序逻辑 模型检测 N皇后问题 TOOLBOX 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]