Hennessy–Milner logic
কম্পিউটার বিজ্ঞানে, হেনেসি-মিলনার লজিক (এইচ. এম. এল) একটি গতিশীল যুক্তি যা একটি লেবেলযুক্ত ট্রানজিশন সিস্টেমের (এল. টি. এস) বৈশিষ্ট্যগুলি নির্দিষ্ট করতে ব্যবহৃত হয়, যা একটি অটোমেটন-এর অনুরূপ একটি কাঠামো। এটি 1980 সালে ম্যাথিউ হেনেসি এবং রবিন মিলনার তাদের গবেষণাপত্রে "অন অবজারভিং ননডেটর্মিনিজম অ্যান্ড কনকারেন্সি" (আইসিএএলপি)-তে প্রবর্তন করেছিলেন। এইচ. এম. এল-এর আরেকটি বৈকল্পিক যুক্তির প্রকাশযোগ্যতা বাড়ানোর জন্য পুনরাবৃত্তির ব্যবহার জড়িত, এবং সাধারণত 'পুনরাবৃত্তির সাথে হেনেসি-মিলনার লজিক' হিসাবে উল্লেখ করা হয়। সর্বাধিক এবং ন্যূনতম স্থির পয়েন্ট ব্যবহার করে পুনরাবৃত্তি সক্ষম করা হয়। বাক্যবিন্যাস একটি সূত্র নিম্নলিখিত বি. এন. এফ ব্যাকরণ দ্বারা সংজ্ঞায়িত করা হয়েছে আইনের জন্য কিছু ক্রিয়ার সেটঃ অর্থাৎ, একটি সূত্র ধ্রুবক সত্য হতে পারে সর্বদা সত্য ধ্রুবক মিথ্যা সর্বদা মিথ্যা সূত্র সংযোগ সূত্র সমস্ত অ্যাক্ট-ডেরিভেটিভের জন্য, φ অবশ্যই কিছু অ্যাক্ট-ডেরিভেটিভের জন্য সূত্র ধারণ করতে হবে, φ অবশ্যই আনুষ্ঠানিক শব্দার্থ ধারণ করতে হবে। সন্তোষজনক সম্পর্কটি এল. টি. এস-এর অবস্থাগুলিকে তাদের সন্তুষ্ট সূত্রের সাথে সম্পর্কিত করে এবং এটিকে ক্ষুদ্রতম সম্পর্ক হিসাবে সংজ্ঞায়িত করা হয় যাতে, সমস্ত অবস্থা এবং সূত্রের জন্য, এমন কোনও অবস্থা না থাকে যার জন্য, যদি এমন কোনও অবস্থা বিদ্যমান থাকে যা এবং তারপর, যদি এমন সবের জন্য যা এটি ধরে রাখে, তাহলে, যদি, তাহলে, যদি, তারপর, যদি, যদি এবং তারপর। এছাড়াও দেখুন মোডাল মাইক্রো-ক্যালকুলাস, যা এইচ. এম. এল-কে নির্দিষ্ট পয়েন্ট অপারেটর ডায়নামিক লজিকের সাথে প্রসারিত করে, যা অসীম অনেক পদ্ধতি সহ একটি মাল্টিমোডাল লজিক। 1988 সালে। "হেনেসি-মিলনার লজিক উইথ রিকার্সন অ্যাজ এ স্পেসিফিকেশন ল্যাঙ্গুয়েজ, অ্যান্ড এ রিফাইনমেন্ট ক্যালকুলাস বেসড অন ইট"। সমবর্তী ব্যবস্থার নির্দিষ্টকরণ এবং যাচাইকরণ সম্পর্কিত বিসিএস-এফএসিএস কর্মশালার কার্যধারায়, চার্লস র্যাট্রে (এড।)। স্প্রিঙ্গার-ভার্লাগ, লন্ডন, যুক্তরাজ্য, 294-330। সমান্তরালতা (কম্পিউটার বিজ্ঞান) আনুষ্ঠানিক নির্দিষ্টকরণ কম্পিউটার বিজ্ঞানে মডেল লজিক লজিক