67پ TAX سازمان امور مالیاتی کشور Proposing a new framework for LTL Model Checking using constraint programming ارائه یک چارچوب مبتنی بر برنامه ریزی قیود جهت بررسی مدل با منطق زمانی خطی 1393 67.پ فارسی کامپیوتر 3 جدول، کتابنامه خیر برنامه نویسی محدودیت فن آوری نرم افزاری نوظهوری برای توصیف اعلانی است و در حل مشکلات بزرگ، به ویژه ترکیبی، خصوصاً در زمینه های برنامه ریزی و زمان بندی موثر است. این شیوه برنامه نویسی بعنوان یکی از زمینه های استراتژیک تحقیقات کامپیوتری شناخته شده که این نه تنها بعلت داشتن پایه قوی نظری بلکه جذب منافع گسترده تجاری و همچنین بطور خاص بهینه سازی مدلسازی ناهمگن و مسائل ارضاء پذیری است. بررسی مدل یک شیوه خودکار جهت بررسی درستی سیستمهای همروند است . در اینجا سیستم همروند بصورت یک گراف حالت-انتقال و مشخصات آن با یک منطق زمانی خاص بیان میگردد.چند نوع منطق زمانی وجود دارد که منطق زمانی خطی و منطق محاسباتی درختی پرکاربردترین آنها هستند. بنابراین ما با استفاده از زبان برنامه ریزی قیود ، مینی زینک چارچوبی جهت بیان مشخصات منطق زمانی خطی در مسئله بررسی مدل ارائه خواهیم نمود.

کلمات کلیدی : بررسی مدل ، برنامه ریزی با قیود ، منطق زمانی خطی ، مینی زینک
  Model checking , Constraint programming , Computation Temporal Logic , Minizinc بررسی مدل ، برنامه ریزی با قیود ، منطق زمانی خطی ، مینی زینک 1789793791